YES 2.437 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ IFR

mainModule List
  ((delete :: (Eq a, Eq b) => Either b a  ->  [Either b a ->  [Either b a]) :: (Eq b, Eq a) => Either b a  ->  [Either b a ->  [Either b a])

module List where
  import qualified Maybe
import qualified Prelude

  delete :: Eq a => a  ->  [a ->  [a]
delete deleteBy (==)

  deleteBy :: (a  ->  a  ->  Bool ->  a  ->  [a ->  [a]
deleteBy _ _ [] []
deleteBy eq x (y : ys if x `eq` y then ys else y : deleteBy eq x ys


module Maybe where
  import qualified List
import qualified Prelude



If Reductions:
The following If expression
if eq x y then ys else y : deleteBy eq x ys

is transformed to
deleteBy0 ys y eq x True = ys
deleteBy0 ys y eq x False = y : deleteBy eq x ys



↳ HASKELL
  ↳ IFR
HASKELL
      ↳ BR

mainModule List
  ((delete :: (Eq b, Eq a) => Either a b  ->  [Either a b ->  [Either a b]) :: (Eq a, Eq b) => Either a b  ->  [Either a b ->  [Either a b])

module List where
  import qualified Maybe
import qualified Prelude

  delete :: Eq a => a  ->  [a ->  [a]
delete deleteBy (==)

  deleteBy :: (a  ->  a  ->  Bool ->  a  ->  [a ->  [a]
deleteBy _ _ [] []
deleteBy eq x (y : ysdeleteBy0 ys y eq x (x `eq` y)

  
deleteBy0 ys y eq x True ys
deleteBy0 ys y eq x False y : deleteBy eq x ys


module Maybe where
  import qualified List
import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ IFR
    ↳ HASKELL
      ↳ BR
HASKELL
          ↳ COR

mainModule List
  ((delete :: (Eq b, Eq a) => Either a b  ->  [Either a b ->  [Either a b]) :: (Eq b, Eq a) => Either a b  ->  [Either a b ->  [Either a b])

module List where
  import qualified Maybe
import qualified Prelude

  delete :: Eq a => a  ->  [a ->  [a]
delete deleteBy (==)

  deleteBy :: (a  ->  a  ->  Bool ->  a  ->  [a ->  [a]
deleteBy vw vx [] []
deleteBy eq x (y : ysdeleteBy0 ys y eq x (x `eq` y)

  
deleteBy0 ys y eq x True ys
deleteBy0 ys y eq x False y : deleteBy eq x ys


module Maybe where
  import qualified List
import qualified Prelude



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ IFR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
HASKELL
              ↳ Narrow

mainModule List
  (delete :: (Eq a, Eq b) => Either b a  ->  [Either b a ->  [Either b a])

module List where
  import qualified Maybe
import qualified Prelude

  delete :: Eq a => a  ->  [a ->  [a]
delete deleteBy (==)

  deleteBy :: (a  ->  a  ->  Bool ->  a  ->  [a ->  [a]
deleteBy vw vx [] []
deleteBy eq x (y : ysdeleteBy0 ys y eq x (x `eq` y)

  
deleteBy0 ys y eq x True ys
deleteBy0 ys y eq x False y : deleteBy eq x ys


module Maybe where
  import qualified List
import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ IFR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
QDP
                    ↳ QDPSizeChangeProof
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(xy2900), Succ(xy4001000)) → new_primPlusNat(xy2900, xy4001000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ IFR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
QDP
                    ↳ QDPSizeChangeProof
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(xy30100), Succ(xy400100)) → new_primMulNat(xy30100, Succ(xy400100))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ IFR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
QDP
                    ↳ QDPSizeChangeProof
                  ↳ QDP
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primEqNat(Succ(xy3000), Succ(xy40000)) → new_primEqNat(xy3000, xy40000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ IFR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
QDP
                    ↳ QDPSizeChangeProof
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_esEs0(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), cc, app(app(ty_@2, ed), ee), dh) → new_esEs1(xy301, xy4001, ed, ee)
new_esEs1(@2(xy300, xy301), @2(xy4000, xy4001), app(app(app(ty_@3, hg), hh), baa), hf) → new_esEs0(xy300, xy4000, hg, hh, baa)
new_esEs3(Right(xy300), Right(xy4000), bdb, app(ty_[], bdc)) → new_esEs(xy300, xy4000, bdc)
new_esEs2(Just(xy300), Just(xy4000), app(ty_[], bag)) → new_esEs(xy300, xy4000, bag)
new_esEs0(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), cc, cd, app(app(ty_Either, de), df)) → new_esEs3(xy302, xy4002, de, df)
new_esEs0(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), app(ty_Maybe, fh), cd, dh) → new_esEs2(xy300, xy4000, fh)
new_esEs0(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), cc, cd, app(ty_Maybe, dd)) → new_esEs2(xy302, xy4002, dd)
new_esEs3(Right(xy300), Right(xy4000), bdb, app(app(ty_Either, beb), bec)) → new_esEs3(xy300, xy4000, beb, bec)
new_esEs3(Left(xy300), Left(xy4000), app(ty_[], bbh), bca) → new_esEs(xy300, xy4000, bbh)
new_esEs0(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), cc, cd, app(ty_[], ce)) → new_esEs(xy302, xy4002, ce)
new_esEs0(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), cc, app(app(app(ty_@3, ea), eb), ec), dh) → new_esEs0(xy301, xy4001, ea, eb, ec)
new_esEs2(Just(xy300), Just(xy4000), app(ty_Maybe, bbe)) → new_esEs2(xy300, xy4000, bbe)
new_esEs3(Right(xy300), Right(xy4000), bdb, app(app(app(ty_@3, bdd), bde), bdf)) → new_esEs0(xy300, xy4000, bdd, bde, bdf)
new_esEs3(Left(xy300), Left(xy4000), app(app(ty_Either, bch), bda), bca) → new_esEs3(xy300, xy4000, bch, bda)
new_esEs2(Just(xy300), Just(xy4000), app(app(ty_@2, bbc), bbd)) → new_esEs1(xy300, xy4000, bbc, bbd)
new_esEs1(@2(xy300, xy301), @2(xy4000, xy4001), gc, app(ty_[], gd)) → new_esEs(xy301, xy4001, gd)
new_esEs1(@2(xy300, xy301), @2(xy4000, xy4001), app(ty_Maybe, bad), hf) → new_esEs2(xy300, xy4000, bad)
new_esEs(:(xy300, xy301), :(xy4000, xy4001), app(ty_Maybe, bh)) → new_esEs2(xy300, xy4000, bh)
new_esEs1(@2(xy300, xy301), @2(xy4000, xy4001), app(ty_[], he), hf) → new_esEs(xy300, xy4000, he)
new_esEs3(Left(xy300), Left(xy4000), app(app(app(ty_@3, bcb), bcc), bcd), bca) → new_esEs0(xy300, xy4000, bcb, bcc, bcd)
new_esEs2(Just(xy300), Just(xy4000), app(app(app(ty_@3, bah), bba), bbb)) → new_esEs0(xy300, xy4000, bah, bba, bbb)
new_esEs1(@2(xy300, xy301), @2(xy4000, xy4001), gc, app(app(ty_Either, hc), hd)) → new_esEs3(xy301, xy4001, hc, hd)
new_esEs(:(xy300, xy301), :(xy4000, xy4001), app(app(ty_@2, bf), bg)) → new_esEs1(xy300, xy4000, bf, bg)
new_esEs1(@2(xy300, xy301), @2(xy4000, xy4001), gc, app(app(ty_@2, gh), ha)) → new_esEs1(xy301, xy4001, gh, ha)
new_esEs0(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), cc, cd, app(app(ty_@2, db), dc)) → new_esEs1(xy302, xy4002, db, dc)
new_esEs3(Left(xy300), Left(xy4000), app(ty_Maybe, bcg), bca) → new_esEs2(xy300, xy4000, bcg)
new_esEs0(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), app(ty_[], fa), cd, dh) → new_esEs(xy300, xy4000, fa)
new_esEs(:(xy300, xy301), :(xy4000, xy4001), ba) → new_esEs(xy301, xy4001, ba)
new_esEs(:(xy300, xy301), :(xy4000, xy4001), app(app(ty_Either, ca), cb)) → new_esEs3(xy300, xy4000, ca, cb)
new_esEs0(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), cc, cd, app(app(app(ty_@3, cf), cg), da)) → new_esEs0(xy302, xy4002, cf, cg, da)
new_esEs0(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), cc, app(ty_[], dg), dh) → new_esEs(xy301, xy4001, dg)
new_esEs3(Left(xy300), Left(xy4000), app(app(ty_@2, bce), bcf), bca) → new_esEs1(xy300, xy4000, bce, bcf)
new_esEs0(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), app(app(ty_Either, ga), gb), cd, dh) → new_esEs3(xy300, xy4000, ga, gb)
new_esEs1(@2(xy300, xy301), @2(xy4000, xy4001), app(app(ty_@2, bab), bac), hf) → new_esEs1(xy300, xy4000, bab, bac)
new_esEs(:(xy300, xy301), :(xy4000, xy4001), app(app(app(ty_@3, bc), bd), be)) → new_esEs0(xy300, xy4000, bc, bd, be)
new_esEs0(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), app(app(ty_@2, ff), fg), cd, dh) → new_esEs1(xy300, xy4000, ff, fg)
new_esEs1(@2(xy300, xy301), @2(xy4000, xy4001), app(app(ty_Either, bae), baf), hf) → new_esEs3(xy300, xy4000, bae, baf)
new_esEs3(Right(xy300), Right(xy4000), bdb, app(ty_Maybe, bea)) → new_esEs2(xy300, xy4000, bea)
new_esEs1(@2(xy300, xy301), @2(xy4000, xy4001), gc, app(ty_Maybe, hb)) → new_esEs2(xy301, xy4001, hb)
new_esEs3(Right(xy300), Right(xy4000), bdb, app(app(ty_@2, bdg), bdh)) → new_esEs1(xy300, xy4000, bdg, bdh)
new_esEs2(Just(xy300), Just(xy4000), app(app(ty_Either, bbf), bbg)) → new_esEs3(xy300, xy4000, bbf, bbg)
new_esEs0(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), cc, app(ty_Maybe, ef), dh) → new_esEs2(xy301, xy4001, ef)
new_esEs0(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), cc, app(app(ty_Either, eg), eh), dh) → new_esEs3(xy301, xy4001, eg, eh)
new_esEs(:(xy300, xy301), :(xy4000, xy4001), app(ty_[], bb)) → new_esEs(xy300, xy4000, bb)
new_esEs1(@2(xy300, xy301), @2(xy4000, xy4001), gc, app(app(app(ty_@3, ge), gf), gg)) → new_esEs0(xy301, xy4001, ge, gf, gg)
new_esEs0(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), app(app(app(ty_@3, fb), fc), fd), cd, dh) → new_esEs0(xy300, xy4000, fb, fc, fd)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ IFR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
QDP
                    ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

new_deleteBy0(xy10, xy11, xy12, False, ba, bb) → new_deleteBy(Left(xy12), xy10, ba, bb)
new_deleteBy(Right(xy30), :(Left(xy400), xy41), bc, bd) → new_deleteBy(Right(xy30), xy41, bc, bd)
new_deleteBy(Left(xy30), :(Left(xy400), xy41), bc, bd) → new_deleteBy0(xy41, xy400, xy30, new_esEs4(xy30, xy400, bc), bc, bd)
new_deleteBy00(xy19, xy20, xy21, False, be, bf) → new_deleteBy(Right(xy21), xy19, be, bf)
new_deleteBy(Right(xy30), :(Right(xy400), xy41), bc, bd) → new_deleteBy00(xy41, xy400, xy30, new_esEs5(xy30, xy400, bd), bc, bd)
new_deleteBy(Left(xy30), :(Right(xy400), xy41), bc, bd) → new_deleteBy(Left(xy30), xy41, bc, bd)

The TRS R consists of the following rules:

new_esEs10(xy301, xy4001, ty_Integer) → new_esEs12(xy301, xy4001)
new_esEs25(xy300, xy4000, ty_Ordering) → new_esEs17(xy300, xy4000)
new_esEs9(xy302, xy4002, app(ty_[], cb)) → new_esEs13(xy302, xy4002, cb)
new_esEs5(xy30, xy400, ty_Double) → new_esEs19(xy30, xy400)
new_primPlusNat1(Succ(xy2900), Succ(xy4001000)) → Succ(Succ(new_primPlusNat1(xy2900, xy4001000)))
new_esEs25(xy300, xy4000, ty_Integer) → new_esEs12(xy300, xy4000)
new_esEs26(xy301, xy4001, ty_Bool) → new_esEs18(xy301, xy4001)
new_esEs22(Left(xy300), Left(xy4000), app(ty_Maybe, bbb), gh) → new_esEs16(xy300, xy4000, bbb)
new_primEqInt(Neg(Succ(xy3000)), Pos(xy4000)) → False
new_primEqInt(Pos(Succ(xy3000)), Neg(xy4000)) → False
new_esEs10(xy301, xy4001, app(app(app(ty_@3, df), dg), dh)) → new_esEs8(xy301, xy4001, df, dg, dh)
new_esEs22(Right(xy300), Right(xy4000), gg, ty_Ordering) → new_esEs17(xy300, xy4000)
new_esEs9(xy302, xy4002, ty_@0) → new_esEs20(xy302, xy4002)
new_esEs5(xy30, xy400, app(app(ty_@2, bdd), bde)) → new_esEs15(xy30, xy400, bdd, bde)
new_esEs5(xy30, xy400, ty_Integer) → new_esEs12(xy30, xy400)
new_esEs22(Left(xy300), Left(xy4000), ty_Float, gh) → new_esEs6(xy300, xy4000)
new_esEs13([], [], gb) → True
new_esEs22(Left(xy300), Left(xy4000), ty_Char, gh) → new_esEs21(xy300, xy4000)
new_esEs9(xy302, xy4002, ty_Float) → new_esEs6(xy302, xy4002)
new_primEqInt(Neg(Zero), Pos(Succ(xy40000))) → False
new_primEqInt(Pos(Zero), Neg(Succ(xy40000))) → False
new_esEs10(xy301, xy4001, ty_Double) → new_esEs19(xy301, xy4001)
new_esEs22(Right(xy300), Right(xy4000), gg, app(app(ty_@2, bcb), bcc)) → new_esEs15(xy300, xy4000, bcb, bcc)
new_esEs16(Just(xy300), Just(xy4000), ty_Ordering) → new_esEs17(xy300, xy4000)
new_esEs26(xy301, xy4001, app(app(ty_@2, bef), beg)) → new_esEs15(xy301, xy4001, bef, beg)
new_esEs16(Just(xy300), Just(xy4000), app(app(app(ty_@3, bgf), bgg), bgh)) → new_esEs8(xy300, xy4000, bgf, bgg, bgh)
new_primMulNat0(Zero, Zero) → Zero
new_esEs16(Nothing, Nothing, gf) → True
new_esEs11(xy300, xy4000, ty_Int) → new_esEs7(xy300, xy4000)
new_esEs11(xy300, xy4000, ty_@0) → new_esEs20(xy300, xy4000)
new_esEs4(xy30, xy400, ty_Int) → new_esEs7(xy30, xy400)
new_esEs4(xy30, xy400, ty_Char) → new_esEs21(xy30, xy400)
new_primPlusNat0(Zero, xy400100) → Succ(xy400100)
new_esEs26(xy301, xy4001, app(ty_Ratio, bee)) → new_esEs14(xy301, xy4001, bee)
new_esEs27(xy300, xy4000, app(app(ty_@2, bfh), bga)) → new_esEs15(xy300, xy4000, bfh, bga)
new_esEs22(Left(xy300), Left(xy4000), ty_@0, gh) → new_esEs20(xy300, xy4000)
new_esEs25(xy300, xy4000, app(app(ty_@2, hf), hg)) → new_esEs15(xy300, xy4000, hf, hg)
new_esEs27(xy300, xy4000, ty_Integer) → new_esEs12(xy300, xy4000)
new_esEs25(xy300, xy4000, ty_Int) → new_esEs7(xy300, xy4000)
new_esEs23(xy301, xy4001, ty_Int) → new_esEs7(xy301, xy4001)
new_esEs22(Left(xy300), Left(xy4000), app(app(ty_Either, bbc), bbd), gh) → new_esEs22(xy300, xy4000, bbc, bbd)
new_esEs22(Left(xy300), Left(xy4000), ty_Int, gh) → new_esEs7(xy300, xy4000)
new_esEs11(xy300, xy4000, ty_Char) → new_esEs21(xy300, xy4000)
new_esEs26(xy301, xy4001, ty_Float) → new_esEs6(xy301, xy4001)
new_esEs24(xy300, xy4000, ty_Integer) → new_esEs12(xy300, xy4000)
new_sr(Pos(xy3010), Neg(xy40010)) → Neg(new_primMulNat0(xy3010, xy40010))
new_sr(Neg(xy3010), Pos(xy40010)) → Neg(new_primMulNat0(xy3010, xy40010))
new_esEs16(Just(xy300), Just(xy4000), ty_Bool) → new_esEs18(xy300, xy4000)
new_esEs11(xy300, xy4000, app(ty_[], eg)) → new_esEs13(xy300, xy4000, eg)
new_esEs4(xy30, xy400, ty_@0) → new_esEs20(xy30, xy400)
new_esEs16(Just(xy300), Just(xy4000), app(ty_Maybe, bhd)) → new_esEs16(xy300, xy4000, bhd)
new_esEs4(xy30, xy400, ty_Float) → new_esEs6(xy30, xy400)
new_esEs11(xy300, xy4000, app(app(ty_@2, fd), ff)) → new_esEs15(xy300, xy4000, fd, ff)
new_esEs8(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), bg, bh, ca) → new_asAs(new_esEs11(xy300, xy4000, bg), new_asAs(new_esEs10(xy301, xy4001, bh), new_esEs9(xy302, xy4002, ca)))
new_esEs4(xy30, xy400, ty_Double) → new_esEs19(xy30, xy400)
new_esEs22(Right(xy300), Right(xy4000), gg, app(ty_Maybe, bcd)) → new_esEs16(xy300, xy4000, bcd)
new_esEs26(xy301, xy4001, app(app(app(ty_@3, beb), bec), bed)) → new_esEs8(xy301, xy4001, beb, bec, bed)
new_esEs16(Just(xy300), Just(xy4000), ty_Char) → new_esEs21(xy300, xy4000)
new_esEs9(xy302, xy4002, ty_Char) → new_esEs21(xy302, xy4002)
new_esEs23(xy301, xy4001, ty_Integer) → new_esEs12(xy301, xy4001)
new_esEs12(Integer(xy300), Integer(xy4000)) → new_primEqInt(xy300, xy4000)
new_esEs11(xy300, xy4000, ty_Bool) → new_esEs18(xy300, xy4000)
new_esEs27(xy300, xy4000, app(app(ty_Either, bgc), bgd)) → new_esEs22(xy300, xy4000, bgc, bgd)
new_esEs25(xy300, xy4000, app(app(ty_Either, baa), bab)) → new_esEs22(xy300, xy4000, baa, bab)
new_primEqNat0(Succ(xy3000), Zero) → False
new_primEqNat0(Zero, Succ(xy40000)) → False
new_esEs4(xy30, xy400, app(ty_Ratio, gc)) → new_esEs14(xy30, xy400, gc)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs10(xy301, xy4001, app(ty_[], de)) → new_esEs13(xy301, xy4001, de)
new_esEs20(@0, @0) → True
new_esEs5(xy30, xy400, ty_Ordering) → new_esEs17(xy30, xy400)
new_esEs22(Left(xy300), Left(xy4000), app(app(ty_@2, bah), bba), gh) → new_esEs15(xy300, xy4000, bah, bba)
new_esEs11(xy300, xy4000, ty_Float) → new_esEs6(xy300, xy4000)
new_esEs5(xy30, xy400, app(ty_[], bcg)) → new_esEs13(xy30, xy400, bcg)
new_esEs22(Left(xy300), Left(xy4000), app(ty_[], bac), gh) → new_esEs13(xy300, xy4000, bac)
new_esEs25(xy300, xy4000, app(app(app(ty_@3, hb), hc), hd)) → new_esEs8(xy300, xy4000, hb, hc, hd)
new_esEs10(xy301, xy4001, ty_Int) → new_esEs7(xy301, xy4001)
new_esEs5(xy30, xy400, ty_Bool) → new_esEs18(xy30, xy400)
new_esEs9(xy302, xy4002, ty_Integer) → new_esEs12(xy302, xy4002)
new_esEs9(xy302, xy4002, app(app(ty_Either, dc), dd)) → new_esEs22(xy302, xy4002, dc, dd)
new_esEs9(xy302, xy4002, app(app(ty_@2, cg), da)) → new_esEs15(xy302, xy4002, cg, da)
new_esEs9(xy302, xy4002, ty_Bool) → new_esEs18(xy302, xy4002)
new_esEs27(xy300, xy4000, app(ty_Maybe, bgb)) → new_esEs16(xy300, xy4000, bgb)
new_esEs24(xy300, xy4000, ty_Int) → new_esEs7(xy300, xy4000)
new_esEs5(xy30, xy400, ty_@0) → new_esEs20(xy30, xy400)
new_esEs22(Right(xy300), Right(xy4000), gg, app(app(app(ty_@3, bbf), bbg), bbh)) → new_esEs8(xy300, xy4000, bbf, bbg, bbh)
new_esEs25(xy300, xy4000, app(ty_Ratio, he)) → new_esEs14(xy300, xy4000, he)
new_esEs4(xy30, xy400, app(app(ty_Either, gg), gh)) → new_esEs22(xy30, xy400, gg, gh)
new_esEs22(Right(xy300), Right(xy4000), gg, ty_Float) → new_esEs6(xy300, xy4000)
new_esEs22(Right(xy300), Right(xy4000), gg, ty_Char) → new_esEs21(xy300, xy4000)
new_esEs16(Just(xy300), Just(xy4000), ty_Integer) → new_esEs12(xy300, xy4000)
new_esEs6(Float(xy300, xy301), Float(xy4000, xy4001)) → new_esEs7(new_sr(xy300, xy4000), new_sr(xy301, xy4001))
new_esEs10(xy301, xy4001, app(ty_Maybe, ed)) → new_esEs16(xy301, xy4001, ed)
new_esEs11(xy300, xy4000, app(ty_Ratio, fc)) → new_esEs14(xy300, xy4000, fc)
new_esEs17(LT, LT) → True
new_esEs27(xy300, xy4000, app(ty_Ratio, bfg)) → new_esEs14(xy300, xy4000, bfg)
new_esEs22(Left(xy300), Left(xy4000), ty_Ordering, gh) → new_esEs17(xy300, xy4000)
new_esEs22(Left(xy300), Left(xy4000), ty_Integer, gh) → new_esEs12(xy300, xy4000)
new_esEs25(xy300, xy4000, ty_Float) → new_esEs6(xy300, xy4000)
new_esEs16(Just(xy300), Just(xy4000), app(app(ty_@2, bhb), bhc)) → new_esEs15(xy300, xy4000, bhb, bhc)
new_esEs9(xy302, xy4002, app(ty_Ratio, cf)) → new_esEs14(xy302, xy4002, cf)
new_sr(Neg(xy3010), Neg(xy40010)) → Pos(new_primMulNat0(xy3010, xy40010))
new_esEs9(xy302, xy4002, ty_Ordering) → new_esEs17(xy302, xy4002)
new_esEs27(xy300, xy4000, ty_Int) → new_esEs7(xy300, xy4000)
new_esEs11(xy300, xy4000, app(app(app(ty_@3, eh), fa), fb)) → new_esEs8(xy300, xy4000, eh, fa, fb)
new_esEs5(xy30, xy400, ty_Int) → new_esEs7(xy30, xy400)
new_asAs(False, xy28) → False
new_sr(Pos(xy3010), Pos(xy40010)) → Pos(new_primMulNat0(xy3010, xy40010))
new_primEqNat0(Zero, Zero) → True
new_esEs4(xy30, xy400, app(app(ty_@2, gd), ge)) → new_esEs15(xy30, xy400, gd, ge)
new_esEs13([], :(xy4000, xy4001), gb) → False
new_esEs13(:(xy300, xy301), [], gb) → False
new_primMulNat0(Succ(xy30100), Zero) → Zero
new_primMulNat0(Zero, Succ(xy400100)) → Zero
new_esEs13(:(xy300, xy301), :(xy4000, xy4001), gb) → new_asAs(new_esEs25(xy300, xy4000, gb), new_esEs13(xy301, xy4001, gb))
new_esEs25(xy300, xy4000, ty_Bool) → new_esEs18(xy300, xy4000)
new_esEs18(True, True) → True
new_esEs7(xy30, xy400) → new_primEqInt(xy30, xy400)
new_esEs16(Just(xy300), Just(xy4000), ty_@0) → new_esEs20(xy300, xy4000)
new_esEs10(xy301, xy4001, ty_@0) → new_esEs20(xy301, xy4001)
new_esEs27(xy300, xy4000, ty_Float) → new_esEs6(xy300, xy4000)
new_esEs5(xy30, xy400, ty_Float) → new_esEs6(xy30, xy400)
new_esEs4(xy30, xy400, ty_Integer) → new_esEs12(xy30, xy400)
new_esEs22(Left(xy300), Left(xy4000), app(ty_Ratio, bag), gh) → new_esEs14(xy300, xy4000, bag)
new_esEs26(xy301, xy4001, ty_Int) → new_esEs7(xy301, xy4001)
new_esEs16(Just(xy300), Just(xy4000), ty_Float) → new_esEs6(xy300, xy4000)
new_esEs27(xy300, xy4000, ty_@0) → new_esEs20(xy300, xy4000)
new_primPlusNat0(Succ(xy290), xy400100) → Succ(Succ(new_primPlusNat1(xy290, xy400100)))
new_esEs25(xy300, xy4000, app(ty_[], ha)) → new_esEs13(xy300, xy4000, ha)
new_esEs11(xy300, xy4000, app(ty_Maybe, fg)) → new_esEs16(xy300, xy4000, fg)
new_esEs10(xy301, xy4001, ty_Ordering) → new_esEs17(xy301, xy4001)
new_esEs5(xy30, xy400, app(ty_Maybe, bdf)) → new_esEs16(xy30, xy400, bdf)
new_esEs17(LT, EQ) → False
new_esEs17(EQ, LT) → False
new_esEs26(xy301, xy4001, ty_Double) → new_esEs19(xy301, xy4001)
new_esEs10(xy301, xy4001, ty_Bool) → new_esEs18(xy301, xy4001)
new_esEs21(Char(xy300), Char(xy4000)) → new_primEqNat0(xy300, xy4000)
new_esEs25(xy300, xy4000, ty_Char) → new_esEs21(xy300, xy4000)
new_esEs4(xy30, xy400, ty_Bool) → new_esEs18(xy30, xy400)
new_esEs26(xy301, xy4001, ty_Integer) → new_esEs12(xy301, xy4001)
new_primEqInt(Neg(Succ(xy3000)), Neg(Succ(xy40000))) → new_primEqNat0(xy3000, xy40000)
new_esEs11(xy300, xy4000, ty_Double) → new_esEs19(xy300, xy4000)
new_esEs16(Just(xy300), Just(xy4000), ty_Int) → new_esEs7(xy300, xy4000)
new_esEs10(xy301, xy4001, ty_Char) → new_esEs21(xy301, xy4001)
new_esEs26(xy301, xy4001, app(ty_[], bea)) → new_esEs13(xy301, xy4001, bea)
new_esEs27(xy300, xy4000, ty_Char) → new_esEs21(xy300, xy4000)
new_primPlusNat1(Zero, Succ(xy4001000)) → Succ(xy4001000)
new_primPlusNat1(Succ(xy2900), Zero) → Succ(xy2900)
new_esEs11(xy300, xy4000, ty_Integer) → new_esEs12(xy300, xy4000)
new_esEs16(Just(xy300), Just(xy4000), app(app(ty_Either, bhe), bhf)) → new_esEs22(xy300, xy4000, bhe, bhf)
new_esEs9(xy302, xy4002, ty_Int) → new_esEs7(xy302, xy4002)
new_esEs26(xy301, xy4001, ty_Ordering) → new_esEs17(xy301, xy4001)
new_esEs26(xy301, xy4001, app(app(ty_Either, bfa), bfb)) → new_esEs22(xy301, xy4001, bfa, bfb)
new_esEs22(Right(xy300), Right(xy4000), gg, ty_Int) → new_esEs7(xy300, xy4000)
new_esEs22(Right(xy300), Right(xy4000), gg, ty_Double) → new_esEs19(xy300, xy4000)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs27(xy300, xy4000, ty_Ordering) → new_esEs17(xy300, xy4000)
new_esEs17(EQ, EQ) → True
new_esEs19(Double(xy300, xy301), Double(xy4000, xy4001)) → new_esEs7(new_sr(xy300, xy4000), new_sr(xy301, xy4001))
new_esEs18(True, False) → False
new_esEs18(False, True) → False
new_esEs16(Nothing, Just(xy4000), gf) → False
new_esEs16(Just(xy300), Nothing, gf) → False
new_primEqInt(Neg(Zero), Neg(Succ(xy40000))) → False
new_primEqInt(Neg(Succ(xy3000)), Neg(Zero)) → False
new_esEs27(xy300, xy4000, ty_Bool) → new_esEs18(xy300, xy4000)
new_esEs26(xy301, xy4001, app(ty_Maybe, beh)) → new_esEs16(xy301, xy4001, beh)
new_esEs10(xy301, xy4001, app(ty_Ratio, ea)) → new_esEs14(xy301, xy4001, ea)
new_esEs25(xy300, xy4000, ty_Double) → new_esEs19(xy300, xy4000)
new_esEs25(xy300, xy4000, app(ty_Maybe, hh)) → new_esEs16(xy300, xy4000, hh)
new_esEs16(Just(xy300), Just(xy4000), app(ty_[], bge)) → new_esEs13(xy300, xy4000, bge)
new_esEs22(Left(xy300), Left(xy4000), ty_Double, gh) → new_esEs19(xy300, xy4000)
new_primPlusNat1(Zero, Zero) → Zero
new_esEs22(Right(xy300), Right(xy4000), gg, ty_Integer) → new_esEs12(xy300, xy4000)
new_asAs(True, xy28) → xy28
new_esEs22(Right(xy300), Right(xy4000), gg, ty_Bool) → new_esEs18(xy300, xy4000)
new_esEs16(Just(xy300), Just(xy4000), ty_Double) → new_esEs19(xy300, xy4000)
new_esEs22(Left(xy300), Left(xy4000), app(app(app(ty_@3, bad), bae), baf), gh) → new_esEs8(xy300, xy4000, bad, bae, baf)
new_primMulNat0(Succ(xy30100), Succ(xy400100)) → new_primPlusNat0(new_primMulNat0(xy30100, Succ(xy400100)), xy400100)
new_esEs27(xy300, xy4000, app(ty_[], bfc)) → new_esEs13(xy300, xy4000, bfc)
new_esEs9(xy302, xy4002, ty_Double) → new_esEs19(xy302, xy4002)
new_esEs9(xy302, xy4002, app(app(app(ty_@3, cc), cd), ce)) → new_esEs8(xy302, xy4002, cc, cd, ce)
new_esEs22(Right(xy300), Right(xy4000), gg, app(ty_Ratio, bca)) → new_esEs14(xy300, xy4000, bca)
new_esEs17(GT, GT) → True
new_esEs14(:%(xy300, xy301), :%(xy4000, xy4001), gc) → new_asAs(new_esEs24(xy300, xy4000, gc), new_esEs23(xy301, xy4001, gc))
new_primEqInt(Pos(Succ(xy3000)), Pos(Succ(xy40000))) → new_primEqNat0(xy3000, xy40000)
new_esEs4(xy30, xy400, app(ty_[], gb)) → new_esEs13(xy30, xy400, gb)
new_esEs11(xy300, xy4000, ty_Ordering) → new_esEs17(xy300, xy4000)
new_esEs22(Left(xy300), Left(xy4000), ty_Bool, gh) → new_esEs18(xy300, xy4000)
new_esEs10(xy301, xy4001, app(app(ty_Either, ee), ef)) → new_esEs22(xy301, xy4001, ee, ef)
new_esEs22(Right(xy300), Left(xy4000), gg, gh) → False
new_esEs22(Left(xy300), Right(xy4000), gg, gh) → False
new_esEs5(xy30, xy400, app(app(ty_Either, bdg), bdh)) → new_esEs22(xy30, xy400, bdg, bdh)
new_esEs17(LT, GT) → False
new_esEs17(GT, LT) → False
new_primEqNat0(Succ(xy3000), Succ(xy40000)) → new_primEqNat0(xy3000, xy40000)
new_esEs4(xy30, xy400, app(ty_Maybe, gf)) → new_esEs16(xy30, xy400, gf)
new_esEs17(EQ, GT) → False
new_esEs17(GT, EQ) → False
new_esEs27(xy300, xy4000, app(app(app(ty_@3, bfd), bfe), bff)) → new_esEs8(xy300, xy4000, bfd, bfe, bff)
new_esEs22(Right(xy300), Right(xy4000), gg, ty_@0) → new_esEs20(xy300, xy4000)
new_esEs26(xy301, xy4001, ty_@0) → new_esEs20(xy301, xy4001)
new_esEs10(xy301, xy4001, app(app(ty_@2, eb), ec)) → new_esEs15(xy301, xy4001, eb, ec)
new_esEs11(xy300, xy4000, app(app(ty_Either, fh), ga)) → new_esEs22(xy300, xy4000, fh, ga)
new_esEs9(xy302, xy4002, app(ty_Maybe, db)) → new_esEs16(xy302, xy4002, db)
new_esEs25(xy300, xy4000, ty_@0) → new_esEs20(xy300, xy4000)
new_esEs16(Just(xy300), Just(xy4000), app(ty_Ratio, bha)) → new_esEs14(xy300, xy4000, bha)
new_esEs10(xy301, xy4001, ty_Float) → new_esEs6(xy301, xy4001)
new_esEs5(xy30, xy400, app(ty_Ratio, bdc)) → new_esEs14(xy30, xy400, bdc)
new_esEs4(xy30, xy400, ty_Ordering) → new_esEs17(xy30, xy400)
new_esEs5(xy30, xy400, ty_Char) → new_esEs21(xy30, xy400)
new_esEs5(xy30, xy400, app(app(app(ty_@3, bch), bda), bdb)) → new_esEs8(xy30, xy400, bch, bda, bdb)
new_primEqInt(Pos(Succ(xy3000)), Pos(Zero)) → False
new_primEqInt(Pos(Zero), Pos(Succ(xy40000))) → False
new_esEs26(xy301, xy4001, ty_Char) → new_esEs21(xy301, xy4001)
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_esEs22(Right(xy300), Right(xy4000), gg, app(app(ty_Either, bce), bcf)) → new_esEs22(xy300, xy4000, bce, bcf)
new_esEs4(xy30, xy400, app(app(app(ty_@3, bg), bh), ca)) → new_esEs8(xy30, xy400, bg, bh, ca)
new_esEs15(@2(xy300, xy301), @2(xy4000, xy4001), gd, ge) → new_asAs(new_esEs27(xy300, xy4000, gd), new_esEs26(xy301, xy4001, ge))
new_esEs22(Right(xy300), Right(xy4000), gg, app(ty_[], bbe)) → new_esEs13(xy300, xy4000, bbe)
new_esEs18(False, False) → True
new_esEs27(xy300, xy4000, ty_Double) → new_esEs19(xy300, xy4000)

The set Q consists of the following terms:

new_esEs10(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs17(LT, GT)
new_esEs17(GT, LT)
new_esEs27(x0, x1, app(app(ty_@2, x2), x3))
new_esEs4(x0, x1, app(ty_[], x2))
new_esEs27(x0, x1, app(ty_[], x2))
new_esEs12(Integer(x0), Integer(x1))
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs11(x0, x1, ty_Bool)
new_esEs5(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs22(Right(x0), Right(x1), x2, ty_@0)
new_esEs4(x0, x1, ty_Bool)
new_esEs16(Just(x0), Just(x1), app(ty_Maybe, x2))
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_esEs27(x0, x1, ty_@0)
new_esEs22(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs22(Right(x0), Right(x1), x2, ty_Int)
new_esEs17(LT, LT)
new_esEs27(x0, x1, ty_Float)
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_esEs16(Just(x0), Just(x1), ty_Ordering)
new_esEs14(:%(x0, x1), :%(x2, x3), x4)
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs9(x0, x1, ty_Int)
new_esEs4(x0, x1, ty_Double)
new_esEs10(x0, x1, ty_Ordering)
new_esEs18(False, True)
new_esEs18(True, False)
new_asAs(False, x0)
new_esEs10(x0, x1, app(app(ty_Either, x2), x3))
new_primPlusNat1(Succ(x0), Zero)
new_esEs9(x0, x1, ty_Bool)
new_esEs5(x0, x1, ty_Bool)
new_esEs25(x0, x1, ty_Double)
new_esEs16(Just(x0), Just(x1), app(ty_[], x2))
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs5(x0, x1, app(ty_Ratio, x2))
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs4(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_Integer)
new_esEs7(x0, x1)
new_esEs9(x0, x1, ty_Integer)
new_esEs22(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs11(x0, x1, ty_Ordering)
new_esEs13([], [], x0)
new_esEs9(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs17(EQ, GT)
new_esEs17(GT, EQ)
new_esEs22(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs22(Left(x0), Left(x1), ty_Double, x2)
new_esEs9(x0, x1, app(app(ty_@2, x2), x3))
new_esEs11(x0, x1, ty_Float)
new_esEs9(x0, x1, app(ty_Ratio, x2))
new_esEs11(x0, x1, app(app(ty_@2, x2), x3))
new_esEs22(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs27(x0, x1, ty_Integer)
new_esEs5(x0, x1, app(ty_Maybe, x2))
new_esEs27(x0, x1, ty_Ordering)
new_esEs18(True, True)
new_esEs26(x0, x1, ty_Double)
new_esEs26(x0, x1, ty_Integer)
new_primPlusNat1(Zero, Succ(x0))
new_esEs16(Just(x0), Just(x1), ty_Double)
new_primPlusNat0(Zero, x0)
new_esEs25(x0, x1, ty_Float)
new_esEs26(x0, x1, ty_Int)
new_esEs10(x0, x1, app(ty_Maybe, x2))
new_esEs16(Nothing, Nothing, x0)
new_esEs8(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_asAs(True, x0)
new_esEs25(x0, x1, ty_Bool)
new_esEs16(Just(x0), Just(x1), ty_Float)
new_esEs5(x0, x1, app(ty_[], x2))
new_esEs17(GT, GT)
new_esEs25(x0, x1, ty_Int)
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_esEs4(x0, x1, ty_Char)
new_esEs11(x0, x1, ty_Int)
new_esEs27(x0, x1, ty_Int)
new_esEs4(x0, x1, ty_Integer)
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs25(x0, x1, ty_Integer)
new_esEs9(x0, x1, ty_Double)
new_esEs22(Right(x0), Right(x1), x2, ty_Bool)
new_esEs26(x0, x1, ty_Bool)
new_esEs25(x0, x1, ty_Char)
new_sr(Pos(x0), Pos(x1))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs22(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs10(x0, x1, app(app(ty_@2, x2), x3))
new_primEqNat0(Zero, Zero)
new_esEs24(x0, x1, ty_Int)
new_esEs24(x0, x1, ty_Integer)
new_esEs22(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs4(x0, x1, ty_Float)
new_esEs9(x0, x1, ty_Char)
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs22(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs16(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs22(Right(x0), Right(x1), x2, ty_Float)
new_primEqNat0(Zero, Succ(x0))
new_esEs10(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_Int)
new_esEs22(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs10(x0, x1, ty_Char)
new_esEs6(Float(x0, x1), Float(x2, x3))
new_esEs27(x0, x1, app(ty_Ratio, x2))
new_esEs11(x0, x1, app(app(ty_Either, x2), x3))
new_esEs13(:(x0, x1), [], x2)
new_esEs22(Left(x0), Left(x1), ty_@0, x2)
new_esEs5(x0, x1, ty_Double)
new_esEs9(x0, x1, ty_@0)
new_primMulNat0(Zero, Zero)
new_esEs25(x0, x1, ty_@0)
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs19(Double(x0, x1), Double(x2, x3))
new_esEs22(Left(x0), Left(x1), ty_Bool, x2)
new_esEs22(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs9(x0, x1, ty_Float)
new_esEs26(x0, x1, ty_Char)
new_esEs9(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs5(x0, x1, ty_@0)
new_esEs16(Just(x0), Just(x1), ty_@0)
new_esEs9(x0, x1, ty_Ordering)
new_esEs13([], :(x0, x1), x2)
new_esEs10(x0, x1, ty_Float)
new_esEs27(x0, x1, app(ty_Maybe, x2))
new_esEs5(x0, x1, app(app(ty_Either, x2), x3))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs22(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs11(x0, x1, app(ty_[], x2))
new_esEs16(Nothing, Just(x0), x1)
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_esEs9(x0, x1, app(ty_Maybe, x2))
new_esEs26(x0, x1, app(ty_[], x2))
new_esEs10(x0, x1, app(ty_Ratio, x2))
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs27(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, ty_Ordering)
new_esEs22(Left(x0), Left(x1), ty_Integer, x2)
new_esEs16(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_esEs21(Char(x0), Char(x1))
new_esEs15(@2(x0, x1), @2(x2, x3), x4, x5)
new_primMulNat0(Zero, Succ(x0))
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs11(x0, x1, ty_Char)
new_esEs22(Right(x0), Right(x1), x2, ty_Integer)
new_esEs27(x0, x1, ty_Char)
new_esEs11(x0, x1, ty_@0)
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs5(x0, x1, app(app(ty_@2, x2), x3))
new_esEs16(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs22(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs22(Left(x0), Left(x1), ty_Char, x2)
new_esEs16(Just(x0), Just(x1), ty_Integer)
new_esEs10(x0, x1, ty_Integer)
new_esEs18(False, False)
new_esEs27(x0, x1, ty_Double)
new_esEs20(@0, @0)
new_esEs16(Just(x0), Just(x1), ty_Int)
new_esEs22(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs4(x0, x1, ty_Ordering)
new_esEs22(Right(x0), Right(x1), x2, ty_Char)
new_esEs11(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs26(x0, x1, ty_@0)
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs22(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs13(:(x0, x1), :(x2, x3), x4)
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs11(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs10(x0, x1, ty_Bool)
new_primEqNat0(Succ(x0), Zero)
new_sr(Neg(x0), Neg(x1))
new_esEs10(x0, x1, ty_Double)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_esEs5(x0, x1, ty_Integer)
new_primPlusNat1(Zero, Zero)
new_esEs5(x0, x1, ty_Ordering)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs27(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(Left(x0), Left(x1), ty_Int, x2)
new_esEs4(x0, x1, ty_Int)
new_esEs16(Just(x0), Nothing, x1)
new_esEs5(x0, x1, ty_Char)
new_esEs22(Left(x0), Right(x1), x2, x3)
new_esEs22(Right(x0), Left(x1), x2, x3)
new_primEqInt(Pos(Zero), Pos(Zero))
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs11(x0, x1, app(ty_Maybe, x2))
new_primPlusNat0(Succ(x0), x1)
new_esEs26(x0, x1, ty_Ordering)
new_esEs5(x0, x1, ty_Float)
new_esEs22(Right(x0), Right(x1), x2, ty_Double)
new_esEs17(EQ, EQ)
new_esEs17(EQ, LT)
new_esEs17(LT, EQ)
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs11(x0, x1, ty_Double)
new_esEs16(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs22(Left(x0), Left(x1), ty_Float, x2)
new_esEs10(x0, x1, ty_Int)
new_esEs16(Just(x0), Just(x1), ty_Bool)
new_esEs5(x0, x1, ty_Int)
new_esEs9(x0, x1, app(ty_[], x2))
new_esEs26(x0, x1, ty_Float)
new_esEs27(x0, x1, ty_Bool)
new_primMulNat0(Succ(x0), Zero)
new_esEs10(x0, x1, app(ty_[], x2))
new_esEs11(x0, x1, ty_Integer)
new_esEs16(Just(x0), Just(x1), ty_Char)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs.

↳ HASKELL
  ↳ IFR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ DependencyGraphProof
                      ↳ AND
QDP
                          ↳ UsableRulesProof
                        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_deleteBy(Right(xy30), :(Left(xy400), xy41), bc, bd) → new_deleteBy(Right(xy30), xy41, bc, bd)
new_deleteBy00(xy19, xy20, xy21, False, be, bf) → new_deleteBy(Right(xy21), xy19, be, bf)
new_deleteBy(Right(xy30), :(Right(xy400), xy41), bc, bd) → new_deleteBy00(xy41, xy400, xy30, new_esEs5(xy30, xy400, bd), bc, bd)

The TRS R consists of the following rules:

new_esEs10(xy301, xy4001, ty_Integer) → new_esEs12(xy301, xy4001)
new_esEs25(xy300, xy4000, ty_Ordering) → new_esEs17(xy300, xy4000)
new_esEs9(xy302, xy4002, app(ty_[], cb)) → new_esEs13(xy302, xy4002, cb)
new_esEs5(xy30, xy400, ty_Double) → new_esEs19(xy30, xy400)
new_primPlusNat1(Succ(xy2900), Succ(xy4001000)) → Succ(Succ(new_primPlusNat1(xy2900, xy4001000)))
new_esEs25(xy300, xy4000, ty_Integer) → new_esEs12(xy300, xy4000)
new_esEs26(xy301, xy4001, ty_Bool) → new_esEs18(xy301, xy4001)
new_esEs22(Left(xy300), Left(xy4000), app(ty_Maybe, bbb), gh) → new_esEs16(xy300, xy4000, bbb)
new_primEqInt(Neg(Succ(xy3000)), Pos(xy4000)) → False
new_primEqInt(Pos(Succ(xy3000)), Neg(xy4000)) → False
new_esEs10(xy301, xy4001, app(app(app(ty_@3, df), dg), dh)) → new_esEs8(xy301, xy4001, df, dg, dh)
new_esEs22(Right(xy300), Right(xy4000), gg, ty_Ordering) → new_esEs17(xy300, xy4000)
new_esEs9(xy302, xy4002, ty_@0) → new_esEs20(xy302, xy4002)
new_esEs5(xy30, xy400, app(app(ty_@2, bdd), bde)) → new_esEs15(xy30, xy400, bdd, bde)
new_esEs5(xy30, xy400, ty_Integer) → new_esEs12(xy30, xy400)
new_esEs22(Left(xy300), Left(xy4000), ty_Float, gh) → new_esEs6(xy300, xy4000)
new_esEs13([], [], gb) → True
new_esEs22(Left(xy300), Left(xy4000), ty_Char, gh) → new_esEs21(xy300, xy4000)
new_esEs9(xy302, xy4002, ty_Float) → new_esEs6(xy302, xy4002)
new_primEqInt(Neg(Zero), Pos(Succ(xy40000))) → False
new_primEqInt(Pos(Zero), Neg(Succ(xy40000))) → False
new_esEs10(xy301, xy4001, ty_Double) → new_esEs19(xy301, xy4001)
new_esEs22(Right(xy300), Right(xy4000), gg, app(app(ty_@2, bcb), bcc)) → new_esEs15(xy300, xy4000, bcb, bcc)
new_esEs16(Just(xy300), Just(xy4000), ty_Ordering) → new_esEs17(xy300, xy4000)
new_esEs26(xy301, xy4001, app(app(ty_@2, bef), beg)) → new_esEs15(xy301, xy4001, bef, beg)
new_esEs16(Just(xy300), Just(xy4000), app(app(app(ty_@3, bgf), bgg), bgh)) → new_esEs8(xy300, xy4000, bgf, bgg, bgh)
new_primMulNat0(Zero, Zero) → Zero
new_esEs16(Nothing, Nothing, gf) → True
new_esEs11(xy300, xy4000, ty_Int) → new_esEs7(xy300, xy4000)
new_esEs11(xy300, xy4000, ty_@0) → new_esEs20(xy300, xy4000)
new_esEs4(xy30, xy400, ty_Int) → new_esEs7(xy30, xy400)
new_esEs4(xy30, xy400, ty_Char) → new_esEs21(xy30, xy400)
new_primPlusNat0(Zero, xy400100) → Succ(xy400100)
new_esEs26(xy301, xy4001, app(ty_Ratio, bee)) → new_esEs14(xy301, xy4001, bee)
new_esEs27(xy300, xy4000, app(app(ty_@2, bfh), bga)) → new_esEs15(xy300, xy4000, bfh, bga)
new_esEs22(Left(xy300), Left(xy4000), ty_@0, gh) → new_esEs20(xy300, xy4000)
new_esEs25(xy300, xy4000, app(app(ty_@2, hf), hg)) → new_esEs15(xy300, xy4000, hf, hg)
new_esEs27(xy300, xy4000, ty_Integer) → new_esEs12(xy300, xy4000)
new_esEs25(xy300, xy4000, ty_Int) → new_esEs7(xy300, xy4000)
new_esEs23(xy301, xy4001, ty_Int) → new_esEs7(xy301, xy4001)
new_esEs22(Left(xy300), Left(xy4000), app(app(ty_Either, bbc), bbd), gh) → new_esEs22(xy300, xy4000, bbc, bbd)
new_esEs22(Left(xy300), Left(xy4000), ty_Int, gh) → new_esEs7(xy300, xy4000)
new_esEs11(xy300, xy4000, ty_Char) → new_esEs21(xy300, xy4000)
new_esEs26(xy301, xy4001, ty_Float) → new_esEs6(xy301, xy4001)
new_esEs24(xy300, xy4000, ty_Integer) → new_esEs12(xy300, xy4000)
new_sr(Pos(xy3010), Neg(xy40010)) → Neg(new_primMulNat0(xy3010, xy40010))
new_sr(Neg(xy3010), Pos(xy40010)) → Neg(new_primMulNat0(xy3010, xy40010))
new_esEs16(Just(xy300), Just(xy4000), ty_Bool) → new_esEs18(xy300, xy4000)
new_esEs11(xy300, xy4000, app(ty_[], eg)) → new_esEs13(xy300, xy4000, eg)
new_esEs4(xy30, xy400, ty_@0) → new_esEs20(xy30, xy400)
new_esEs16(Just(xy300), Just(xy4000), app(ty_Maybe, bhd)) → new_esEs16(xy300, xy4000, bhd)
new_esEs4(xy30, xy400, ty_Float) → new_esEs6(xy30, xy400)
new_esEs11(xy300, xy4000, app(app(ty_@2, fd), ff)) → new_esEs15(xy300, xy4000, fd, ff)
new_esEs8(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), bg, bh, ca) → new_asAs(new_esEs11(xy300, xy4000, bg), new_asAs(new_esEs10(xy301, xy4001, bh), new_esEs9(xy302, xy4002, ca)))
new_esEs4(xy30, xy400, ty_Double) → new_esEs19(xy30, xy400)
new_esEs22(Right(xy300), Right(xy4000), gg, app(ty_Maybe, bcd)) → new_esEs16(xy300, xy4000, bcd)
new_esEs26(xy301, xy4001, app(app(app(ty_@3, beb), bec), bed)) → new_esEs8(xy301, xy4001, beb, bec, bed)
new_esEs16(Just(xy300), Just(xy4000), ty_Char) → new_esEs21(xy300, xy4000)
new_esEs9(xy302, xy4002, ty_Char) → new_esEs21(xy302, xy4002)
new_esEs23(xy301, xy4001, ty_Integer) → new_esEs12(xy301, xy4001)
new_esEs12(Integer(xy300), Integer(xy4000)) → new_primEqInt(xy300, xy4000)
new_esEs11(xy300, xy4000, ty_Bool) → new_esEs18(xy300, xy4000)
new_esEs27(xy300, xy4000, app(app(ty_Either, bgc), bgd)) → new_esEs22(xy300, xy4000, bgc, bgd)
new_esEs25(xy300, xy4000, app(app(ty_Either, baa), bab)) → new_esEs22(xy300, xy4000, baa, bab)
new_primEqNat0(Succ(xy3000), Zero) → False
new_primEqNat0(Zero, Succ(xy40000)) → False
new_esEs4(xy30, xy400, app(ty_Ratio, gc)) → new_esEs14(xy30, xy400, gc)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs10(xy301, xy4001, app(ty_[], de)) → new_esEs13(xy301, xy4001, de)
new_esEs20(@0, @0) → True
new_esEs5(xy30, xy400, ty_Ordering) → new_esEs17(xy30, xy400)
new_esEs22(Left(xy300), Left(xy4000), app(app(ty_@2, bah), bba), gh) → new_esEs15(xy300, xy4000, bah, bba)
new_esEs11(xy300, xy4000, ty_Float) → new_esEs6(xy300, xy4000)
new_esEs5(xy30, xy400, app(ty_[], bcg)) → new_esEs13(xy30, xy400, bcg)
new_esEs22(Left(xy300), Left(xy4000), app(ty_[], bac), gh) → new_esEs13(xy300, xy4000, bac)
new_esEs25(xy300, xy4000, app(app(app(ty_@3, hb), hc), hd)) → new_esEs8(xy300, xy4000, hb, hc, hd)
new_esEs10(xy301, xy4001, ty_Int) → new_esEs7(xy301, xy4001)
new_esEs5(xy30, xy400, ty_Bool) → new_esEs18(xy30, xy400)
new_esEs9(xy302, xy4002, ty_Integer) → new_esEs12(xy302, xy4002)
new_esEs9(xy302, xy4002, app(app(ty_Either, dc), dd)) → new_esEs22(xy302, xy4002, dc, dd)
new_esEs9(xy302, xy4002, app(app(ty_@2, cg), da)) → new_esEs15(xy302, xy4002, cg, da)
new_esEs9(xy302, xy4002, ty_Bool) → new_esEs18(xy302, xy4002)
new_esEs27(xy300, xy4000, app(ty_Maybe, bgb)) → new_esEs16(xy300, xy4000, bgb)
new_esEs24(xy300, xy4000, ty_Int) → new_esEs7(xy300, xy4000)
new_esEs5(xy30, xy400, ty_@0) → new_esEs20(xy30, xy400)
new_esEs22(Right(xy300), Right(xy4000), gg, app(app(app(ty_@3, bbf), bbg), bbh)) → new_esEs8(xy300, xy4000, bbf, bbg, bbh)
new_esEs25(xy300, xy4000, app(ty_Ratio, he)) → new_esEs14(xy300, xy4000, he)
new_esEs4(xy30, xy400, app(app(ty_Either, gg), gh)) → new_esEs22(xy30, xy400, gg, gh)
new_esEs22(Right(xy300), Right(xy4000), gg, ty_Float) → new_esEs6(xy300, xy4000)
new_esEs22(Right(xy300), Right(xy4000), gg, ty_Char) → new_esEs21(xy300, xy4000)
new_esEs16(Just(xy300), Just(xy4000), ty_Integer) → new_esEs12(xy300, xy4000)
new_esEs6(Float(xy300, xy301), Float(xy4000, xy4001)) → new_esEs7(new_sr(xy300, xy4000), new_sr(xy301, xy4001))
new_esEs10(xy301, xy4001, app(ty_Maybe, ed)) → new_esEs16(xy301, xy4001, ed)
new_esEs11(xy300, xy4000, app(ty_Ratio, fc)) → new_esEs14(xy300, xy4000, fc)
new_esEs17(LT, LT) → True
new_esEs27(xy300, xy4000, app(ty_Ratio, bfg)) → new_esEs14(xy300, xy4000, bfg)
new_esEs22(Left(xy300), Left(xy4000), ty_Ordering, gh) → new_esEs17(xy300, xy4000)
new_esEs22(Left(xy300), Left(xy4000), ty_Integer, gh) → new_esEs12(xy300, xy4000)
new_esEs25(xy300, xy4000, ty_Float) → new_esEs6(xy300, xy4000)
new_esEs16(Just(xy300), Just(xy4000), app(app(ty_@2, bhb), bhc)) → new_esEs15(xy300, xy4000, bhb, bhc)
new_esEs9(xy302, xy4002, app(ty_Ratio, cf)) → new_esEs14(xy302, xy4002, cf)
new_sr(Neg(xy3010), Neg(xy40010)) → Pos(new_primMulNat0(xy3010, xy40010))
new_esEs9(xy302, xy4002, ty_Ordering) → new_esEs17(xy302, xy4002)
new_esEs27(xy300, xy4000, ty_Int) → new_esEs7(xy300, xy4000)
new_esEs11(xy300, xy4000, app(app(app(ty_@3, eh), fa), fb)) → new_esEs8(xy300, xy4000, eh, fa, fb)
new_esEs5(xy30, xy400, ty_Int) → new_esEs7(xy30, xy400)
new_asAs(False, xy28) → False
new_sr(Pos(xy3010), Pos(xy40010)) → Pos(new_primMulNat0(xy3010, xy40010))
new_primEqNat0(Zero, Zero) → True
new_esEs4(xy30, xy400, app(app(ty_@2, gd), ge)) → new_esEs15(xy30, xy400, gd, ge)
new_esEs13([], :(xy4000, xy4001), gb) → False
new_esEs13(:(xy300, xy301), [], gb) → False
new_primMulNat0(Succ(xy30100), Zero) → Zero
new_primMulNat0(Zero, Succ(xy400100)) → Zero
new_esEs13(:(xy300, xy301), :(xy4000, xy4001), gb) → new_asAs(new_esEs25(xy300, xy4000, gb), new_esEs13(xy301, xy4001, gb))
new_esEs25(xy300, xy4000, ty_Bool) → new_esEs18(xy300, xy4000)
new_esEs18(True, True) → True
new_esEs7(xy30, xy400) → new_primEqInt(xy30, xy400)
new_esEs16(Just(xy300), Just(xy4000), ty_@0) → new_esEs20(xy300, xy4000)
new_esEs10(xy301, xy4001, ty_@0) → new_esEs20(xy301, xy4001)
new_esEs27(xy300, xy4000, ty_Float) → new_esEs6(xy300, xy4000)
new_esEs5(xy30, xy400, ty_Float) → new_esEs6(xy30, xy400)
new_esEs4(xy30, xy400, ty_Integer) → new_esEs12(xy30, xy400)
new_esEs22(Left(xy300), Left(xy4000), app(ty_Ratio, bag), gh) → new_esEs14(xy300, xy4000, bag)
new_esEs26(xy301, xy4001, ty_Int) → new_esEs7(xy301, xy4001)
new_esEs16(Just(xy300), Just(xy4000), ty_Float) → new_esEs6(xy300, xy4000)
new_esEs27(xy300, xy4000, ty_@0) → new_esEs20(xy300, xy4000)
new_primPlusNat0(Succ(xy290), xy400100) → Succ(Succ(new_primPlusNat1(xy290, xy400100)))
new_esEs25(xy300, xy4000, app(ty_[], ha)) → new_esEs13(xy300, xy4000, ha)
new_esEs11(xy300, xy4000, app(ty_Maybe, fg)) → new_esEs16(xy300, xy4000, fg)
new_esEs10(xy301, xy4001, ty_Ordering) → new_esEs17(xy301, xy4001)
new_esEs5(xy30, xy400, app(ty_Maybe, bdf)) → new_esEs16(xy30, xy400, bdf)
new_esEs17(LT, EQ) → False
new_esEs17(EQ, LT) → False
new_esEs26(xy301, xy4001, ty_Double) → new_esEs19(xy301, xy4001)
new_esEs10(xy301, xy4001, ty_Bool) → new_esEs18(xy301, xy4001)
new_esEs21(Char(xy300), Char(xy4000)) → new_primEqNat0(xy300, xy4000)
new_esEs25(xy300, xy4000, ty_Char) → new_esEs21(xy300, xy4000)
new_esEs4(xy30, xy400, ty_Bool) → new_esEs18(xy30, xy400)
new_esEs26(xy301, xy4001, ty_Integer) → new_esEs12(xy301, xy4001)
new_primEqInt(Neg(Succ(xy3000)), Neg(Succ(xy40000))) → new_primEqNat0(xy3000, xy40000)
new_esEs11(xy300, xy4000, ty_Double) → new_esEs19(xy300, xy4000)
new_esEs16(Just(xy300), Just(xy4000), ty_Int) → new_esEs7(xy300, xy4000)
new_esEs10(xy301, xy4001, ty_Char) → new_esEs21(xy301, xy4001)
new_esEs26(xy301, xy4001, app(ty_[], bea)) → new_esEs13(xy301, xy4001, bea)
new_esEs27(xy300, xy4000, ty_Char) → new_esEs21(xy300, xy4000)
new_primPlusNat1(Zero, Succ(xy4001000)) → Succ(xy4001000)
new_primPlusNat1(Succ(xy2900), Zero) → Succ(xy2900)
new_esEs11(xy300, xy4000, ty_Integer) → new_esEs12(xy300, xy4000)
new_esEs16(Just(xy300), Just(xy4000), app(app(ty_Either, bhe), bhf)) → new_esEs22(xy300, xy4000, bhe, bhf)
new_esEs9(xy302, xy4002, ty_Int) → new_esEs7(xy302, xy4002)
new_esEs26(xy301, xy4001, ty_Ordering) → new_esEs17(xy301, xy4001)
new_esEs26(xy301, xy4001, app(app(ty_Either, bfa), bfb)) → new_esEs22(xy301, xy4001, bfa, bfb)
new_esEs22(Right(xy300), Right(xy4000), gg, ty_Int) → new_esEs7(xy300, xy4000)
new_esEs22(Right(xy300), Right(xy4000), gg, ty_Double) → new_esEs19(xy300, xy4000)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs27(xy300, xy4000, ty_Ordering) → new_esEs17(xy300, xy4000)
new_esEs17(EQ, EQ) → True
new_esEs19(Double(xy300, xy301), Double(xy4000, xy4001)) → new_esEs7(new_sr(xy300, xy4000), new_sr(xy301, xy4001))
new_esEs18(True, False) → False
new_esEs18(False, True) → False
new_esEs16(Nothing, Just(xy4000), gf) → False
new_esEs16(Just(xy300), Nothing, gf) → False
new_primEqInt(Neg(Zero), Neg(Succ(xy40000))) → False
new_primEqInt(Neg(Succ(xy3000)), Neg(Zero)) → False
new_esEs27(xy300, xy4000, ty_Bool) → new_esEs18(xy300, xy4000)
new_esEs26(xy301, xy4001, app(ty_Maybe, beh)) → new_esEs16(xy301, xy4001, beh)
new_esEs10(xy301, xy4001, app(ty_Ratio, ea)) → new_esEs14(xy301, xy4001, ea)
new_esEs25(xy300, xy4000, ty_Double) → new_esEs19(xy300, xy4000)
new_esEs25(xy300, xy4000, app(ty_Maybe, hh)) → new_esEs16(xy300, xy4000, hh)
new_esEs16(Just(xy300), Just(xy4000), app(ty_[], bge)) → new_esEs13(xy300, xy4000, bge)
new_esEs22(Left(xy300), Left(xy4000), ty_Double, gh) → new_esEs19(xy300, xy4000)
new_primPlusNat1(Zero, Zero) → Zero
new_esEs22(Right(xy300), Right(xy4000), gg, ty_Integer) → new_esEs12(xy300, xy4000)
new_asAs(True, xy28) → xy28
new_esEs22(Right(xy300), Right(xy4000), gg, ty_Bool) → new_esEs18(xy300, xy4000)
new_esEs16(Just(xy300), Just(xy4000), ty_Double) → new_esEs19(xy300, xy4000)
new_esEs22(Left(xy300), Left(xy4000), app(app(app(ty_@3, bad), bae), baf), gh) → new_esEs8(xy300, xy4000, bad, bae, baf)
new_primMulNat0(Succ(xy30100), Succ(xy400100)) → new_primPlusNat0(new_primMulNat0(xy30100, Succ(xy400100)), xy400100)
new_esEs27(xy300, xy4000, app(ty_[], bfc)) → new_esEs13(xy300, xy4000, bfc)
new_esEs9(xy302, xy4002, ty_Double) → new_esEs19(xy302, xy4002)
new_esEs9(xy302, xy4002, app(app(app(ty_@3, cc), cd), ce)) → new_esEs8(xy302, xy4002, cc, cd, ce)
new_esEs22(Right(xy300), Right(xy4000), gg, app(ty_Ratio, bca)) → new_esEs14(xy300, xy4000, bca)
new_esEs17(GT, GT) → True
new_esEs14(:%(xy300, xy301), :%(xy4000, xy4001), gc) → new_asAs(new_esEs24(xy300, xy4000, gc), new_esEs23(xy301, xy4001, gc))
new_primEqInt(Pos(Succ(xy3000)), Pos(Succ(xy40000))) → new_primEqNat0(xy3000, xy40000)
new_esEs4(xy30, xy400, app(ty_[], gb)) → new_esEs13(xy30, xy400, gb)
new_esEs11(xy300, xy4000, ty_Ordering) → new_esEs17(xy300, xy4000)
new_esEs22(Left(xy300), Left(xy4000), ty_Bool, gh) → new_esEs18(xy300, xy4000)
new_esEs10(xy301, xy4001, app(app(ty_Either, ee), ef)) → new_esEs22(xy301, xy4001, ee, ef)
new_esEs22(Right(xy300), Left(xy4000), gg, gh) → False
new_esEs22(Left(xy300), Right(xy4000), gg, gh) → False
new_esEs5(xy30, xy400, app(app(ty_Either, bdg), bdh)) → new_esEs22(xy30, xy400, bdg, bdh)
new_esEs17(LT, GT) → False
new_esEs17(GT, LT) → False
new_primEqNat0(Succ(xy3000), Succ(xy40000)) → new_primEqNat0(xy3000, xy40000)
new_esEs4(xy30, xy400, app(ty_Maybe, gf)) → new_esEs16(xy30, xy400, gf)
new_esEs17(EQ, GT) → False
new_esEs17(GT, EQ) → False
new_esEs27(xy300, xy4000, app(app(app(ty_@3, bfd), bfe), bff)) → new_esEs8(xy300, xy4000, bfd, bfe, bff)
new_esEs22(Right(xy300), Right(xy4000), gg, ty_@0) → new_esEs20(xy300, xy4000)
new_esEs26(xy301, xy4001, ty_@0) → new_esEs20(xy301, xy4001)
new_esEs10(xy301, xy4001, app(app(ty_@2, eb), ec)) → new_esEs15(xy301, xy4001, eb, ec)
new_esEs11(xy300, xy4000, app(app(ty_Either, fh), ga)) → new_esEs22(xy300, xy4000, fh, ga)
new_esEs9(xy302, xy4002, app(ty_Maybe, db)) → new_esEs16(xy302, xy4002, db)
new_esEs25(xy300, xy4000, ty_@0) → new_esEs20(xy300, xy4000)
new_esEs16(Just(xy300), Just(xy4000), app(ty_Ratio, bha)) → new_esEs14(xy300, xy4000, bha)
new_esEs10(xy301, xy4001, ty_Float) → new_esEs6(xy301, xy4001)
new_esEs5(xy30, xy400, app(ty_Ratio, bdc)) → new_esEs14(xy30, xy400, bdc)
new_esEs4(xy30, xy400, ty_Ordering) → new_esEs17(xy30, xy400)
new_esEs5(xy30, xy400, ty_Char) → new_esEs21(xy30, xy400)
new_esEs5(xy30, xy400, app(app(app(ty_@3, bch), bda), bdb)) → new_esEs8(xy30, xy400, bch, bda, bdb)
new_primEqInt(Pos(Succ(xy3000)), Pos(Zero)) → False
new_primEqInt(Pos(Zero), Pos(Succ(xy40000))) → False
new_esEs26(xy301, xy4001, ty_Char) → new_esEs21(xy301, xy4001)
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_esEs22(Right(xy300), Right(xy4000), gg, app(app(ty_Either, bce), bcf)) → new_esEs22(xy300, xy4000, bce, bcf)
new_esEs4(xy30, xy400, app(app(app(ty_@3, bg), bh), ca)) → new_esEs8(xy30, xy400, bg, bh, ca)
new_esEs15(@2(xy300, xy301), @2(xy4000, xy4001), gd, ge) → new_asAs(new_esEs27(xy300, xy4000, gd), new_esEs26(xy301, xy4001, ge))
new_esEs22(Right(xy300), Right(xy4000), gg, app(ty_[], bbe)) → new_esEs13(xy300, xy4000, bbe)
new_esEs18(False, False) → True
new_esEs27(xy300, xy4000, ty_Double) → new_esEs19(xy300, xy4000)

The set Q consists of the following terms:

new_esEs10(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs17(LT, GT)
new_esEs17(GT, LT)
new_esEs27(x0, x1, app(app(ty_@2, x2), x3))
new_esEs4(x0, x1, app(ty_[], x2))
new_esEs27(x0, x1, app(ty_[], x2))
new_esEs12(Integer(x0), Integer(x1))
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs11(x0, x1, ty_Bool)
new_esEs5(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs22(Right(x0), Right(x1), x2, ty_@0)
new_esEs4(x0, x1, ty_Bool)
new_esEs16(Just(x0), Just(x1), app(ty_Maybe, x2))
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_esEs27(x0, x1, ty_@0)
new_esEs22(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs22(Right(x0), Right(x1), x2, ty_Int)
new_esEs17(LT, LT)
new_esEs27(x0, x1, ty_Float)
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_esEs16(Just(x0), Just(x1), ty_Ordering)
new_esEs14(:%(x0, x1), :%(x2, x3), x4)
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs9(x0, x1, ty_Int)
new_esEs4(x0, x1, ty_Double)
new_esEs10(x0, x1, ty_Ordering)
new_esEs18(False, True)
new_esEs18(True, False)
new_asAs(False, x0)
new_esEs10(x0, x1, app(app(ty_Either, x2), x3))
new_primPlusNat1(Succ(x0), Zero)
new_esEs9(x0, x1, ty_Bool)
new_esEs5(x0, x1, ty_Bool)
new_esEs25(x0, x1, ty_Double)
new_esEs16(Just(x0), Just(x1), app(ty_[], x2))
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs5(x0, x1, app(ty_Ratio, x2))
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs4(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_Integer)
new_esEs7(x0, x1)
new_esEs9(x0, x1, ty_Integer)
new_esEs22(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs11(x0, x1, ty_Ordering)
new_esEs13([], [], x0)
new_esEs9(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs17(EQ, GT)
new_esEs17(GT, EQ)
new_esEs22(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs22(Left(x0), Left(x1), ty_Double, x2)
new_esEs9(x0, x1, app(app(ty_@2, x2), x3))
new_esEs11(x0, x1, ty_Float)
new_esEs9(x0, x1, app(ty_Ratio, x2))
new_esEs11(x0, x1, app(app(ty_@2, x2), x3))
new_esEs22(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs27(x0, x1, ty_Integer)
new_esEs5(x0, x1, app(ty_Maybe, x2))
new_esEs27(x0, x1, ty_Ordering)
new_esEs18(True, True)
new_esEs26(x0, x1, ty_Double)
new_esEs26(x0, x1, ty_Integer)
new_primPlusNat1(Zero, Succ(x0))
new_esEs16(Just(x0), Just(x1), ty_Double)
new_primPlusNat0(Zero, x0)
new_esEs25(x0, x1, ty_Float)
new_esEs26(x0, x1, ty_Int)
new_esEs10(x0, x1, app(ty_Maybe, x2))
new_esEs16(Nothing, Nothing, x0)
new_esEs8(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_asAs(True, x0)
new_esEs25(x0, x1, ty_Bool)
new_esEs16(Just(x0), Just(x1), ty_Float)
new_esEs5(x0, x1, app(ty_[], x2))
new_esEs17(GT, GT)
new_esEs25(x0, x1, ty_Int)
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_esEs4(x0, x1, ty_Char)
new_esEs11(x0, x1, ty_Int)
new_esEs27(x0, x1, ty_Int)
new_esEs4(x0, x1, ty_Integer)
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs25(x0, x1, ty_Integer)
new_esEs9(x0, x1, ty_Double)
new_esEs22(Right(x0), Right(x1), x2, ty_Bool)
new_esEs26(x0, x1, ty_Bool)
new_esEs25(x0, x1, ty_Char)
new_sr(Pos(x0), Pos(x1))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs22(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs10(x0, x1, app(app(ty_@2, x2), x3))
new_primEqNat0(Zero, Zero)
new_esEs24(x0, x1, ty_Int)
new_esEs24(x0, x1, ty_Integer)
new_esEs22(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs4(x0, x1, ty_Float)
new_esEs9(x0, x1, ty_Char)
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs22(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs16(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs22(Right(x0), Right(x1), x2, ty_Float)
new_primEqNat0(Zero, Succ(x0))
new_esEs10(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_Int)
new_esEs22(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs10(x0, x1, ty_Char)
new_esEs6(Float(x0, x1), Float(x2, x3))
new_esEs27(x0, x1, app(ty_Ratio, x2))
new_esEs11(x0, x1, app(app(ty_Either, x2), x3))
new_esEs13(:(x0, x1), [], x2)
new_esEs22(Left(x0), Left(x1), ty_@0, x2)
new_esEs5(x0, x1, ty_Double)
new_esEs9(x0, x1, ty_@0)
new_primMulNat0(Zero, Zero)
new_esEs25(x0, x1, ty_@0)
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs19(Double(x0, x1), Double(x2, x3))
new_esEs22(Left(x0), Left(x1), ty_Bool, x2)
new_esEs22(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs9(x0, x1, ty_Float)
new_esEs26(x0, x1, ty_Char)
new_esEs9(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs5(x0, x1, ty_@0)
new_esEs16(Just(x0), Just(x1), ty_@0)
new_esEs9(x0, x1, ty_Ordering)
new_esEs13([], :(x0, x1), x2)
new_esEs10(x0, x1, ty_Float)
new_esEs27(x0, x1, app(ty_Maybe, x2))
new_esEs5(x0, x1, app(app(ty_Either, x2), x3))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs22(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs11(x0, x1, app(ty_[], x2))
new_esEs16(Nothing, Just(x0), x1)
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_esEs9(x0, x1, app(ty_Maybe, x2))
new_esEs26(x0, x1, app(ty_[], x2))
new_esEs10(x0, x1, app(ty_Ratio, x2))
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs27(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, ty_Ordering)
new_esEs22(Left(x0), Left(x1), ty_Integer, x2)
new_esEs16(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_esEs21(Char(x0), Char(x1))
new_esEs15(@2(x0, x1), @2(x2, x3), x4, x5)
new_primMulNat0(Zero, Succ(x0))
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs11(x0, x1, ty_Char)
new_esEs22(Right(x0), Right(x1), x2, ty_Integer)
new_esEs27(x0, x1, ty_Char)
new_esEs11(x0, x1, ty_@0)
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs5(x0, x1, app(app(ty_@2, x2), x3))
new_esEs16(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs22(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs22(Left(x0), Left(x1), ty_Char, x2)
new_esEs16(Just(x0), Just(x1), ty_Integer)
new_esEs10(x0, x1, ty_Integer)
new_esEs18(False, False)
new_esEs27(x0, x1, ty_Double)
new_esEs20(@0, @0)
new_esEs16(Just(x0), Just(x1), ty_Int)
new_esEs22(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs4(x0, x1, ty_Ordering)
new_esEs22(Right(x0), Right(x1), x2, ty_Char)
new_esEs11(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs26(x0, x1, ty_@0)
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs22(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs13(:(x0, x1), :(x2, x3), x4)
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs11(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs10(x0, x1, ty_Bool)
new_primEqNat0(Succ(x0), Zero)
new_sr(Neg(x0), Neg(x1))
new_esEs10(x0, x1, ty_Double)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_esEs5(x0, x1, ty_Integer)
new_primPlusNat1(Zero, Zero)
new_esEs5(x0, x1, ty_Ordering)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs27(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(Left(x0), Left(x1), ty_Int, x2)
new_esEs4(x0, x1, ty_Int)
new_esEs16(Just(x0), Nothing, x1)
new_esEs5(x0, x1, ty_Char)
new_esEs22(Left(x0), Right(x1), x2, x3)
new_esEs22(Right(x0), Left(x1), x2, x3)
new_primEqInt(Pos(Zero), Pos(Zero))
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs11(x0, x1, app(ty_Maybe, x2))
new_primPlusNat0(Succ(x0), x1)
new_esEs26(x0, x1, ty_Ordering)
new_esEs5(x0, x1, ty_Float)
new_esEs22(Right(x0), Right(x1), x2, ty_Double)
new_esEs17(EQ, EQ)
new_esEs17(EQ, LT)
new_esEs17(LT, EQ)
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs11(x0, x1, ty_Double)
new_esEs16(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs22(Left(x0), Left(x1), ty_Float, x2)
new_esEs10(x0, x1, ty_Int)
new_esEs16(Just(x0), Just(x1), ty_Bool)
new_esEs5(x0, x1, ty_Int)
new_esEs9(x0, x1, app(ty_[], x2))
new_esEs26(x0, x1, ty_Float)
new_esEs27(x0, x1, ty_Bool)
new_primMulNat0(Succ(x0), Zero)
new_esEs10(x0, x1, app(ty_[], x2))
new_esEs11(x0, x1, ty_Integer)
new_esEs16(Just(x0), Just(x1), ty_Char)

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL
  ↳ IFR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ DependencyGraphProof
                      ↳ AND
                        ↳ QDP
                          ↳ UsableRulesProof
QDP
                              ↳ QReductionProof
                        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_deleteBy(Right(xy30), :(Left(xy400), xy41), bc, bd) → new_deleteBy(Right(xy30), xy41, bc, bd)
new_deleteBy00(xy19, xy20, xy21, False, be, bf) → new_deleteBy(Right(xy21), xy19, be, bf)
new_deleteBy(Right(xy30), :(Right(xy400), xy41), bc, bd) → new_deleteBy00(xy41, xy400, xy30, new_esEs5(xy30, xy400, bd), bc, bd)

The TRS R consists of the following rules:

new_esEs5(xy30, xy400, ty_Double) → new_esEs19(xy30, xy400)
new_esEs5(xy30, xy400, app(app(ty_@2, bdd), bde)) → new_esEs15(xy30, xy400, bdd, bde)
new_esEs5(xy30, xy400, ty_Integer) → new_esEs12(xy30, xy400)
new_esEs5(xy30, xy400, ty_Ordering) → new_esEs17(xy30, xy400)
new_esEs5(xy30, xy400, app(ty_[], bcg)) → new_esEs13(xy30, xy400, bcg)
new_esEs5(xy30, xy400, ty_Bool) → new_esEs18(xy30, xy400)
new_esEs5(xy30, xy400, ty_@0) → new_esEs20(xy30, xy400)
new_esEs5(xy30, xy400, ty_Int) → new_esEs7(xy30, xy400)
new_esEs5(xy30, xy400, ty_Float) → new_esEs6(xy30, xy400)
new_esEs5(xy30, xy400, app(ty_Maybe, bdf)) → new_esEs16(xy30, xy400, bdf)
new_esEs5(xy30, xy400, app(app(ty_Either, bdg), bdh)) → new_esEs22(xy30, xy400, bdg, bdh)
new_esEs5(xy30, xy400, app(ty_Ratio, bdc)) → new_esEs14(xy30, xy400, bdc)
new_esEs5(xy30, xy400, ty_Char) → new_esEs21(xy30, xy400)
new_esEs5(xy30, xy400, app(app(app(ty_@3, bch), bda), bdb)) → new_esEs8(xy30, xy400, bch, bda, bdb)
new_esEs8(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), bg, bh, ca) → new_asAs(new_esEs11(xy300, xy4000, bg), new_asAs(new_esEs10(xy301, xy4001, bh), new_esEs9(xy302, xy4002, ca)))
new_esEs11(xy300, xy4000, ty_Int) → new_esEs7(xy300, xy4000)
new_esEs11(xy300, xy4000, ty_@0) → new_esEs20(xy300, xy4000)
new_esEs11(xy300, xy4000, ty_Char) → new_esEs21(xy300, xy4000)
new_esEs11(xy300, xy4000, app(ty_[], eg)) → new_esEs13(xy300, xy4000, eg)
new_esEs11(xy300, xy4000, app(app(ty_@2, fd), ff)) → new_esEs15(xy300, xy4000, fd, ff)
new_esEs11(xy300, xy4000, ty_Bool) → new_esEs18(xy300, xy4000)
new_esEs11(xy300, xy4000, ty_Float) → new_esEs6(xy300, xy4000)
new_esEs11(xy300, xy4000, app(ty_Ratio, fc)) → new_esEs14(xy300, xy4000, fc)
new_esEs11(xy300, xy4000, app(app(app(ty_@3, eh), fa), fb)) → new_esEs8(xy300, xy4000, eh, fa, fb)
new_esEs11(xy300, xy4000, app(ty_Maybe, fg)) → new_esEs16(xy300, xy4000, fg)
new_esEs11(xy300, xy4000, ty_Double) → new_esEs19(xy300, xy4000)
new_esEs11(xy300, xy4000, ty_Integer) → new_esEs12(xy300, xy4000)
new_esEs11(xy300, xy4000, ty_Ordering) → new_esEs17(xy300, xy4000)
new_esEs11(xy300, xy4000, app(app(ty_Either, fh), ga)) → new_esEs22(xy300, xy4000, fh, ga)
new_esEs10(xy301, xy4001, ty_Integer) → new_esEs12(xy301, xy4001)
new_esEs10(xy301, xy4001, app(app(app(ty_@3, df), dg), dh)) → new_esEs8(xy301, xy4001, df, dg, dh)
new_esEs10(xy301, xy4001, ty_Double) → new_esEs19(xy301, xy4001)
new_esEs10(xy301, xy4001, app(ty_[], de)) → new_esEs13(xy301, xy4001, de)
new_esEs10(xy301, xy4001, ty_Int) → new_esEs7(xy301, xy4001)
new_esEs10(xy301, xy4001, app(ty_Maybe, ed)) → new_esEs16(xy301, xy4001, ed)
new_esEs10(xy301, xy4001, ty_@0) → new_esEs20(xy301, xy4001)
new_esEs10(xy301, xy4001, ty_Ordering) → new_esEs17(xy301, xy4001)
new_esEs10(xy301, xy4001, ty_Bool) → new_esEs18(xy301, xy4001)
new_esEs10(xy301, xy4001, ty_Char) → new_esEs21(xy301, xy4001)
new_esEs10(xy301, xy4001, app(ty_Ratio, ea)) → new_esEs14(xy301, xy4001, ea)
new_esEs10(xy301, xy4001, app(app(ty_Either, ee), ef)) → new_esEs22(xy301, xy4001, ee, ef)
new_esEs10(xy301, xy4001, app(app(ty_@2, eb), ec)) → new_esEs15(xy301, xy4001, eb, ec)
new_esEs10(xy301, xy4001, ty_Float) → new_esEs6(xy301, xy4001)
new_esEs9(xy302, xy4002, app(ty_[], cb)) → new_esEs13(xy302, xy4002, cb)
new_esEs9(xy302, xy4002, ty_@0) → new_esEs20(xy302, xy4002)
new_esEs9(xy302, xy4002, ty_Float) → new_esEs6(xy302, xy4002)
new_esEs9(xy302, xy4002, ty_Char) → new_esEs21(xy302, xy4002)
new_esEs9(xy302, xy4002, ty_Integer) → new_esEs12(xy302, xy4002)
new_esEs9(xy302, xy4002, app(app(ty_Either, dc), dd)) → new_esEs22(xy302, xy4002, dc, dd)
new_esEs9(xy302, xy4002, app(app(ty_@2, cg), da)) → new_esEs15(xy302, xy4002, cg, da)
new_esEs9(xy302, xy4002, ty_Bool) → new_esEs18(xy302, xy4002)
new_esEs9(xy302, xy4002, app(ty_Ratio, cf)) → new_esEs14(xy302, xy4002, cf)
new_esEs9(xy302, xy4002, ty_Ordering) → new_esEs17(xy302, xy4002)
new_esEs9(xy302, xy4002, ty_Int) → new_esEs7(xy302, xy4002)
new_esEs9(xy302, xy4002, ty_Double) → new_esEs19(xy302, xy4002)
new_esEs9(xy302, xy4002, app(app(app(ty_@3, cc), cd), ce)) → new_esEs8(xy302, xy4002, cc, cd, ce)
new_esEs9(xy302, xy4002, app(ty_Maybe, db)) → new_esEs16(xy302, xy4002, db)
new_asAs(False, xy28) → False
new_asAs(True, xy28) → xy28
new_esEs16(Just(xy300), Just(xy4000), ty_Ordering) → new_esEs17(xy300, xy4000)
new_esEs16(Just(xy300), Just(xy4000), app(app(app(ty_@3, bgf), bgg), bgh)) → new_esEs8(xy300, xy4000, bgf, bgg, bgh)
new_esEs16(Nothing, Nothing, gf) → True
new_esEs16(Just(xy300), Just(xy4000), ty_Bool) → new_esEs18(xy300, xy4000)
new_esEs22(Right(xy300), Right(xy4000), gg, app(app(ty_Either, bce), bcf)) → new_esEs22(xy300, xy4000, bce, bcf)
new_esEs22(Right(xy300), Right(xy4000), gg, app(ty_Maybe, bcd)) → new_esEs16(xy300, xy4000, bcd)
new_esEs22(Left(xy300), Left(xy4000), app(app(ty_Either, bbc), bbd), gh) → new_esEs22(xy300, xy4000, bbc, bbd)
new_esEs22(Left(xy300), Left(xy4000), app(ty_Maybe, bbb), gh) → new_esEs16(xy300, xy4000, bbb)
new_esEs16(Just(xy300), Just(xy4000), app(ty_Maybe, bhd)) → new_esEs16(xy300, xy4000, bhd)
new_esEs16(Just(xy300), Just(xy4000), app(app(ty_Either, bhe), bhf)) → new_esEs22(xy300, xy4000, bhe, bhf)
new_esEs16(Just(xy300), Just(xy4000), ty_Char) → new_esEs21(xy300, xy4000)
new_esEs16(Just(xy300), Just(xy4000), ty_Integer) → new_esEs12(xy300, xy4000)
new_esEs16(Just(xy300), Just(xy4000), app(app(ty_@2, bhb), bhc)) → new_esEs15(xy300, xy4000, bhb, bhc)
new_esEs16(Just(xy300), Just(xy4000), ty_@0) → new_esEs20(xy300, xy4000)
new_esEs16(Just(xy300), Just(xy4000), ty_Float) → new_esEs6(xy300, xy4000)
new_esEs16(Just(xy300), Just(xy4000), ty_Int) → new_esEs7(xy300, xy4000)
new_esEs16(Nothing, Just(xy4000), gf) → False
new_esEs16(Just(xy300), Nothing, gf) → False
new_esEs16(Just(xy300), Just(xy4000), app(ty_[], bge)) → new_esEs13(xy300, xy4000, bge)
new_esEs16(Just(xy300), Just(xy4000), ty_Double) → new_esEs19(xy300, xy4000)
new_esEs16(Just(xy300), Just(xy4000), app(ty_Ratio, bha)) → new_esEs14(xy300, xy4000, bha)
new_esEs14(:%(xy300, xy301), :%(xy4000, xy4001), gc) → new_asAs(new_esEs24(xy300, xy4000, gc), new_esEs23(xy301, xy4001, gc))
new_esEs24(xy300, xy4000, ty_Integer) → new_esEs12(xy300, xy4000)
new_esEs24(xy300, xy4000, ty_Int) → new_esEs7(xy300, xy4000)
new_esEs23(xy301, xy4001, ty_Int) → new_esEs7(xy301, xy4001)
new_esEs23(xy301, xy4001, ty_Integer) → new_esEs12(xy301, xy4001)
new_esEs12(Integer(xy300), Integer(xy4000)) → new_primEqInt(xy300, xy4000)
new_primEqInt(Neg(Succ(xy3000)), Pos(xy4000)) → False
new_primEqInt(Pos(Succ(xy3000)), Neg(xy4000)) → False
new_primEqInt(Neg(Zero), Pos(Succ(xy40000))) → False
new_primEqInt(Pos(Zero), Neg(Succ(xy40000))) → False
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_primEqInt(Neg(Succ(xy3000)), Neg(Succ(xy40000))) → new_primEqNat0(xy3000, xy40000)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_primEqInt(Neg(Zero), Neg(Succ(xy40000))) → False
new_primEqInt(Neg(Succ(xy3000)), Neg(Zero)) → False
new_primEqInt(Pos(Succ(xy3000)), Pos(Succ(xy40000))) → new_primEqNat0(xy3000, xy40000)
new_primEqInt(Pos(Succ(xy3000)), Pos(Zero)) → False
new_primEqInt(Pos(Zero), Pos(Succ(xy40000))) → False
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_primEqNat0(Succ(xy3000), Zero) → False
new_primEqNat0(Zero, Succ(xy40000)) → False
new_primEqNat0(Zero, Zero) → True
new_primEqNat0(Succ(xy3000), Succ(xy40000)) → new_primEqNat0(xy3000, xy40000)
new_esEs7(xy30, xy400) → new_primEqInt(xy30, xy400)
new_esEs19(Double(xy300, xy301), Double(xy4000, xy4001)) → new_esEs7(new_sr(xy300, xy4000), new_sr(xy301, xy4001))
new_sr(Pos(xy3010), Neg(xy40010)) → Neg(new_primMulNat0(xy3010, xy40010))
new_sr(Neg(xy3010), Pos(xy40010)) → Neg(new_primMulNat0(xy3010, xy40010))
new_sr(Neg(xy3010), Neg(xy40010)) → Pos(new_primMulNat0(xy3010, xy40010))
new_sr(Pos(xy3010), Pos(xy40010)) → Pos(new_primMulNat0(xy3010, xy40010))
new_primMulNat0(Zero, Zero) → Zero
new_primMulNat0(Succ(xy30100), Zero) → Zero
new_primMulNat0(Zero, Succ(xy400100)) → Zero
new_primMulNat0(Succ(xy30100), Succ(xy400100)) → new_primPlusNat0(new_primMulNat0(xy30100, Succ(xy400100)), xy400100)
new_primPlusNat0(Zero, xy400100) → Succ(xy400100)
new_primPlusNat0(Succ(xy290), xy400100) → Succ(Succ(new_primPlusNat1(xy290, xy400100)))
new_primPlusNat1(Succ(xy2900), Succ(xy4001000)) → Succ(Succ(new_primPlusNat1(xy2900, xy4001000)))
new_primPlusNat1(Zero, Succ(xy4001000)) → Succ(xy4001000)
new_primPlusNat1(Succ(xy2900), Zero) → Succ(xy2900)
new_primPlusNat1(Zero, Zero) → Zero
new_esEs13([], [], gb) → True
new_esEs13([], :(xy4000, xy4001), gb) → False
new_esEs13(:(xy300, xy301), [], gb) → False
new_esEs13(:(xy300, xy301), :(xy4000, xy4001), gb) → new_asAs(new_esEs25(xy300, xy4000, gb), new_esEs13(xy301, xy4001, gb))
new_esEs25(xy300, xy4000, ty_Ordering) → new_esEs17(xy300, xy4000)
new_esEs25(xy300, xy4000, ty_Integer) → new_esEs12(xy300, xy4000)
new_esEs25(xy300, xy4000, app(app(ty_@2, hf), hg)) → new_esEs15(xy300, xy4000, hf, hg)
new_esEs25(xy300, xy4000, ty_Int) → new_esEs7(xy300, xy4000)
new_esEs25(xy300, xy4000, app(app(ty_Either, baa), bab)) → new_esEs22(xy300, xy4000, baa, bab)
new_esEs25(xy300, xy4000, app(app(app(ty_@3, hb), hc), hd)) → new_esEs8(xy300, xy4000, hb, hc, hd)
new_esEs25(xy300, xy4000, app(ty_Ratio, he)) → new_esEs14(xy300, xy4000, he)
new_esEs25(xy300, xy4000, ty_Float) → new_esEs6(xy300, xy4000)
new_esEs25(xy300, xy4000, ty_Bool) → new_esEs18(xy300, xy4000)
new_esEs25(xy300, xy4000, app(ty_[], ha)) → new_esEs13(xy300, xy4000, ha)
new_esEs25(xy300, xy4000, ty_Char) → new_esEs21(xy300, xy4000)
new_esEs25(xy300, xy4000, ty_Double) → new_esEs19(xy300, xy4000)
new_esEs25(xy300, xy4000, app(ty_Maybe, hh)) → new_esEs16(xy300, xy4000, hh)
new_esEs25(xy300, xy4000, ty_@0) → new_esEs20(xy300, xy4000)
new_esEs20(@0, @0) → True
new_esEs21(Char(xy300), Char(xy4000)) → new_primEqNat0(xy300, xy4000)
new_esEs18(True, True) → True
new_esEs18(True, False) → False
new_esEs18(False, True) → False
new_esEs18(False, False) → True
new_esEs6(Float(xy300, xy301), Float(xy4000, xy4001)) → new_esEs7(new_sr(xy300, xy4000), new_sr(xy301, xy4001))
new_esEs22(Right(xy300), Right(xy4000), gg, ty_Ordering) → new_esEs17(xy300, xy4000)
new_esEs22(Left(xy300), Left(xy4000), ty_Float, gh) → new_esEs6(xy300, xy4000)
new_esEs22(Left(xy300), Left(xy4000), ty_Char, gh) → new_esEs21(xy300, xy4000)
new_esEs22(Right(xy300), Right(xy4000), gg, app(app(ty_@2, bcb), bcc)) → new_esEs15(xy300, xy4000, bcb, bcc)
new_esEs22(Left(xy300), Left(xy4000), ty_@0, gh) → new_esEs20(xy300, xy4000)
new_esEs22(Left(xy300), Left(xy4000), ty_Int, gh) → new_esEs7(xy300, xy4000)
new_esEs22(Left(xy300), Left(xy4000), app(app(ty_@2, bah), bba), gh) → new_esEs15(xy300, xy4000, bah, bba)
new_esEs22(Left(xy300), Left(xy4000), app(ty_[], bac), gh) → new_esEs13(xy300, xy4000, bac)
new_esEs22(Right(xy300), Right(xy4000), gg, app(app(app(ty_@3, bbf), bbg), bbh)) → new_esEs8(xy300, xy4000, bbf, bbg, bbh)
new_esEs22(Right(xy300), Right(xy4000), gg, ty_Float) → new_esEs6(xy300, xy4000)
new_esEs22(Right(xy300), Right(xy4000), gg, ty_Char) → new_esEs21(xy300, xy4000)
new_esEs22(Left(xy300), Left(xy4000), ty_Ordering, gh) → new_esEs17(xy300, xy4000)
new_esEs22(Left(xy300), Left(xy4000), ty_Integer, gh) → new_esEs12(xy300, xy4000)
new_esEs22(Left(xy300), Left(xy4000), app(ty_Ratio, bag), gh) → new_esEs14(xy300, xy4000, bag)
new_esEs22(Right(xy300), Right(xy4000), gg, ty_Int) → new_esEs7(xy300, xy4000)
new_esEs22(Right(xy300), Right(xy4000), gg, ty_Double) → new_esEs19(xy300, xy4000)
new_esEs22(Left(xy300), Left(xy4000), ty_Double, gh) → new_esEs19(xy300, xy4000)
new_esEs22(Right(xy300), Right(xy4000), gg, ty_Integer) → new_esEs12(xy300, xy4000)
new_esEs22(Right(xy300), Right(xy4000), gg, ty_Bool) → new_esEs18(xy300, xy4000)
new_esEs22(Left(xy300), Left(xy4000), app(app(app(ty_@3, bad), bae), baf), gh) → new_esEs8(xy300, xy4000, bad, bae, baf)
new_esEs22(Right(xy300), Right(xy4000), gg, app(ty_Ratio, bca)) → new_esEs14(xy300, xy4000, bca)
new_esEs22(Left(xy300), Left(xy4000), ty_Bool, gh) → new_esEs18(xy300, xy4000)
new_esEs22(Right(xy300), Left(xy4000), gg, gh) → False
new_esEs22(Left(xy300), Right(xy4000), gg, gh) → False
new_esEs22(Right(xy300), Right(xy4000), gg, ty_@0) → new_esEs20(xy300, xy4000)
new_esEs22(Right(xy300), Right(xy4000), gg, app(ty_[], bbe)) → new_esEs13(xy300, xy4000, bbe)
new_esEs17(LT, LT) → True
new_esEs17(LT, EQ) → False
new_esEs17(EQ, LT) → False
new_esEs17(EQ, EQ) → True
new_esEs17(GT, GT) → True
new_esEs17(LT, GT) → False
new_esEs17(GT, LT) → False
new_esEs17(EQ, GT) → False
new_esEs17(GT, EQ) → False
new_esEs15(@2(xy300, xy301), @2(xy4000, xy4001), gd, ge) → new_asAs(new_esEs27(xy300, xy4000, gd), new_esEs26(xy301, xy4001, ge))
new_esEs27(xy300, xy4000, app(app(ty_@2, bfh), bga)) → new_esEs15(xy300, xy4000, bfh, bga)
new_esEs27(xy300, xy4000, ty_Integer) → new_esEs12(xy300, xy4000)
new_esEs27(xy300, xy4000, app(app(ty_Either, bgc), bgd)) → new_esEs22(xy300, xy4000, bgc, bgd)
new_esEs27(xy300, xy4000, app(ty_Maybe, bgb)) → new_esEs16(xy300, xy4000, bgb)
new_esEs27(xy300, xy4000, app(ty_Ratio, bfg)) → new_esEs14(xy300, xy4000, bfg)
new_esEs27(xy300, xy4000, ty_Int) → new_esEs7(xy300, xy4000)
new_esEs27(xy300, xy4000, ty_Float) → new_esEs6(xy300, xy4000)
new_esEs27(xy300, xy4000, ty_@0) → new_esEs20(xy300, xy4000)
new_esEs27(xy300, xy4000, ty_Char) → new_esEs21(xy300, xy4000)
new_esEs27(xy300, xy4000, ty_Ordering) → new_esEs17(xy300, xy4000)
new_esEs27(xy300, xy4000, ty_Bool) → new_esEs18(xy300, xy4000)
new_esEs27(xy300, xy4000, app(ty_[], bfc)) → new_esEs13(xy300, xy4000, bfc)
new_esEs27(xy300, xy4000, app(app(app(ty_@3, bfd), bfe), bff)) → new_esEs8(xy300, xy4000, bfd, bfe, bff)
new_esEs27(xy300, xy4000, ty_Double) → new_esEs19(xy300, xy4000)
new_esEs26(xy301, xy4001, ty_Bool) → new_esEs18(xy301, xy4001)
new_esEs26(xy301, xy4001, app(app(ty_@2, bef), beg)) → new_esEs15(xy301, xy4001, bef, beg)
new_esEs26(xy301, xy4001, app(ty_Ratio, bee)) → new_esEs14(xy301, xy4001, bee)
new_esEs26(xy301, xy4001, ty_Float) → new_esEs6(xy301, xy4001)
new_esEs26(xy301, xy4001, app(app(app(ty_@3, beb), bec), bed)) → new_esEs8(xy301, xy4001, beb, bec, bed)
new_esEs26(xy301, xy4001, ty_Int) → new_esEs7(xy301, xy4001)
new_esEs26(xy301, xy4001, ty_Double) → new_esEs19(xy301, xy4001)
new_esEs26(xy301, xy4001, ty_Integer) → new_esEs12(xy301, xy4001)
new_esEs26(xy301, xy4001, app(ty_[], bea)) → new_esEs13(xy301, xy4001, bea)
new_esEs26(xy301, xy4001, ty_Ordering) → new_esEs17(xy301, xy4001)
new_esEs26(xy301, xy4001, app(app(ty_Either, bfa), bfb)) → new_esEs22(xy301, xy4001, bfa, bfb)
new_esEs26(xy301, xy4001, app(ty_Maybe, beh)) → new_esEs16(xy301, xy4001, beh)
new_esEs26(xy301, xy4001, ty_@0) → new_esEs20(xy301, xy4001)
new_esEs26(xy301, xy4001, ty_Char) → new_esEs21(xy301, xy4001)

The set Q consists of the following terms:

new_esEs10(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs17(LT, GT)
new_esEs17(GT, LT)
new_esEs27(x0, x1, app(app(ty_@2, x2), x3))
new_esEs4(x0, x1, app(ty_[], x2))
new_esEs27(x0, x1, app(ty_[], x2))
new_esEs12(Integer(x0), Integer(x1))
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs11(x0, x1, ty_Bool)
new_esEs5(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs22(Right(x0), Right(x1), x2, ty_@0)
new_esEs4(x0, x1, ty_Bool)
new_esEs16(Just(x0), Just(x1), app(ty_Maybe, x2))
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_esEs27(x0, x1, ty_@0)
new_esEs22(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs22(Right(x0), Right(x1), x2, ty_Int)
new_esEs17(LT, LT)
new_esEs27(x0, x1, ty_Float)
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_esEs16(Just(x0), Just(x1), ty_Ordering)
new_esEs14(:%(x0, x1), :%(x2, x3), x4)
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs9(x0, x1, ty_Int)
new_esEs4(x0, x1, ty_Double)
new_esEs10(x0, x1, ty_Ordering)
new_esEs18(False, True)
new_esEs18(True, False)
new_asAs(False, x0)
new_esEs10(x0, x1, app(app(ty_Either, x2), x3))
new_primPlusNat1(Succ(x0), Zero)
new_esEs9(x0, x1, ty_Bool)
new_esEs5(x0, x1, ty_Bool)
new_esEs25(x0, x1, ty_Double)
new_esEs16(Just(x0), Just(x1), app(ty_[], x2))
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs5(x0, x1, app(ty_Ratio, x2))
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs4(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_Integer)
new_esEs7(x0, x1)
new_esEs9(x0, x1, ty_Integer)
new_esEs22(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs11(x0, x1, ty_Ordering)
new_esEs13([], [], x0)
new_esEs9(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs17(EQ, GT)
new_esEs17(GT, EQ)
new_esEs22(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs22(Left(x0), Left(x1), ty_Double, x2)
new_esEs9(x0, x1, app(app(ty_@2, x2), x3))
new_esEs11(x0, x1, ty_Float)
new_esEs9(x0, x1, app(ty_Ratio, x2))
new_esEs11(x0, x1, app(app(ty_@2, x2), x3))
new_esEs22(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs27(x0, x1, ty_Integer)
new_esEs5(x0, x1, app(ty_Maybe, x2))
new_esEs27(x0, x1, ty_Ordering)
new_esEs18(True, True)
new_esEs26(x0, x1, ty_Double)
new_esEs26(x0, x1, ty_Integer)
new_primPlusNat1(Zero, Succ(x0))
new_esEs16(Just(x0), Just(x1), ty_Double)
new_primPlusNat0(Zero, x0)
new_esEs25(x0, x1, ty_Float)
new_esEs26(x0, x1, ty_Int)
new_esEs10(x0, x1, app(ty_Maybe, x2))
new_esEs16(Nothing, Nothing, x0)
new_esEs8(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_asAs(True, x0)
new_esEs25(x0, x1, ty_Bool)
new_esEs16(Just(x0), Just(x1), ty_Float)
new_esEs5(x0, x1, app(ty_[], x2))
new_esEs17(GT, GT)
new_esEs25(x0, x1, ty_Int)
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_esEs4(x0, x1, ty_Char)
new_esEs11(x0, x1, ty_Int)
new_esEs27(x0, x1, ty_Int)
new_esEs4(x0, x1, ty_Integer)
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs25(x0, x1, ty_Integer)
new_esEs9(x0, x1, ty_Double)
new_esEs22(Right(x0), Right(x1), x2, ty_Bool)
new_esEs26(x0, x1, ty_Bool)
new_esEs25(x0, x1, ty_Char)
new_sr(Pos(x0), Pos(x1))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs22(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs10(x0, x1, app(app(ty_@2, x2), x3))
new_primEqNat0(Zero, Zero)
new_esEs24(x0, x1, ty_Int)
new_esEs24(x0, x1, ty_Integer)
new_esEs22(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs4(x0, x1, ty_Float)
new_esEs9(x0, x1, ty_Char)
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs22(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs16(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs22(Right(x0), Right(x1), x2, ty_Float)
new_primEqNat0(Zero, Succ(x0))
new_esEs10(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_Int)
new_esEs22(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs10(x0, x1, ty_Char)
new_esEs6(Float(x0, x1), Float(x2, x3))
new_esEs27(x0, x1, app(ty_Ratio, x2))
new_esEs11(x0, x1, app(app(ty_Either, x2), x3))
new_esEs13(:(x0, x1), [], x2)
new_esEs22(Left(x0), Left(x1), ty_@0, x2)
new_esEs5(x0, x1, ty_Double)
new_esEs9(x0, x1, ty_@0)
new_primMulNat0(Zero, Zero)
new_esEs25(x0, x1, ty_@0)
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs19(Double(x0, x1), Double(x2, x3))
new_esEs22(Left(x0), Left(x1), ty_Bool, x2)
new_esEs22(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs9(x0, x1, ty_Float)
new_esEs26(x0, x1, ty_Char)
new_esEs9(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs5(x0, x1, ty_@0)
new_esEs16(Just(x0), Just(x1), ty_@0)
new_esEs9(x0, x1, ty_Ordering)
new_esEs13([], :(x0, x1), x2)
new_esEs10(x0, x1, ty_Float)
new_esEs27(x0, x1, app(ty_Maybe, x2))
new_esEs5(x0, x1, app(app(ty_Either, x2), x3))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs22(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs11(x0, x1, app(ty_[], x2))
new_esEs16(Nothing, Just(x0), x1)
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_esEs9(x0, x1, app(ty_Maybe, x2))
new_esEs26(x0, x1, app(ty_[], x2))
new_esEs10(x0, x1, app(ty_Ratio, x2))
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs27(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, ty_Ordering)
new_esEs22(Left(x0), Left(x1), ty_Integer, x2)
new_esEs16(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_esEs21(Char(x0), Char(x1))
new_esEs15(@2(x0, x1), @2(x2, x3), x4, x5)
new_primMulNat0(Zero, Succ(x0))
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs11(x0, x1, ty_Char)
new_esEs22(Right(x0), Right(x1), x2, ty_Integer)
new_esEs27(x0, x1, ty_Char)
new_esEs11(x0, x1, ty_@0)
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs5(x0, x1, app(app(ty_@2, x2), x3))
new_esEs16(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs22(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs22(Left(x0), Left(x1), ty_Char, x2)
new_esEs16(Just(x0), Just(x1), ty_Integer)
new_esEs10(x0, x1, ty_Integer)
new_esEs18(False, False)
new_esEs27(x0, x1, ty_Double)
new_esEs20(@0, @0)
new_esEs16(Just(x0), Just(x1), ty_Int)
new_esEs22(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs4(x0, x1, ty_Ordering)
new_esEs22(Right(x0), Right(x1), x2, ty_Char)
new_esEs11(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs26(x0, x1, ty_@0)
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs22(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs13(:(x0, x1), :(x2, x3), x4)
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs11(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs10(x0, x1, ty_Bool)
new_primEqNat0(Succ(x0), Zero)
new_sr(Neg(x0), Neg(x1))
new_esEs10(x0, x1, ty_Double)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_esEs5(x0, x1, ty_Integer)
new_primPlusNat1(Zero, Zero)
new_esEs5(x0, x1, ty_Ordering)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs27(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(Left(x0), Left(x1), ty_Int, x2)
new_esEs4(x0, x1, ty_Int)
new_esEs16(Just(x0), Nothing, x1)
new_esEs5(x0, x1, ty_Char)
new_esEs22(Left(x0), Right(x1), x2, x3)
new_esEs22(Right(x0), Left(x1), x2, x3)
new_primEqInt(Pos(Zero), Pos(Zero))
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs11(x0, x1, app(ty_Maybe, x2))
new_primPlusNat0(Succ(x0), x1)
new_esEs26(x0, x1, ty_Ordering)
new_esEs5(x0, x1, ty_Float)
new_esEs22(Right(x0), Right(x1), x2, ty_Double)
new_esEs17(EQ, EQ)
new_esEs17(EQ, LT)
new_esEs17(LT, EQ)
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs11(x0, x1, ty_Double)
new_esEs16(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs22(Left(x0), Left(x1), ty_Float, x2)
new_esEs10(x0, x1, ty_Int)
new_esEs16(Just(x0), Just(x1), ty_Bool)
new_esEs5(x0, x1, ty_Int)
new_esEs9(x0, x1, app(ty_[], x2))
new_esEs26(x0, x1, ty_Float)
new_esEs27(x0, x1, ty_Bool)
new_primMulNat0(Succ(x0), Zero)
new_esEs10(x0, x1, app(ty_[], x2))
new_esEs11(x0, x1, ty_Integer)
new_esEs16(Just(x0), Just(x1), ty_Char)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_esEs4(x0, x1, app(ty_[], x2))
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs4(x0, x1, ty_Bool)
new_esEs4(x0, x1, ty_Double)
new_esEs4(x0, x1, ty_@0)
new_esEs4(x0, x1, ty_Char)
new_esEs4(x0, x1, ty_Integer)
new_esEs4(x0, x1, ty_Float)
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs4(x0, x1, ty_Ordering)
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs4(x0, x1, ty_Int)



↳ HASKELL
  ↳ IFR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ DependencyGraphProof
                      ↳ AND
                        ↳ QDP
                          ↳ UsableRulesProof
                            ↳ QDP
                              ↳ QReductionProof
QDP
                                  ↳ QDPSizeChangeProof
                        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_deleteBy(Right(xy30), :(Left(xy400), xy41), bc, bd) → new_deleteBy(Right(xy30), xy41, bc, bd)
new_deleteBy00(xy19, xy20, xy21, False, be, bf) → new_deleteBy(Right(xy21), xy19, be, bf)
new_deleteBy(Right(xy30), :(Right(xy400), xy41), bc, bd) → new_deleteBy00(xy41, xy400, xy30, new_esEs5(xy30, xy400, bd), bc, bd)

The TRS R consists of the following rules:

new_esEs5(xy30, xy400, ty_Double) → new_esEs19(xy30, xy400)
new_esEs5(xy30, xy400, app(app(ty_@2, bdd), bde)) → new_esEs15(xy30, xy400, bdd, bde)
new_esEs5(xy30, xy400, ty_Integer) → new_esEs12(xy30, xy400)
new_esEs5(xy30, xy400, ty_Ordering) → new_esEs17(xy30, xy400)
new_esEs5(xy30, xy400, app(ty_[], bcg)) → new_esEs13(xy30, xy400, bcg)
new_esEs5(xy30, xy400, ty_Bool) → new_esEs18(xy30, xy400)
new_esEs5(xy30, xy400, ty_@0) → new_esEs20(xy30, xy400)
new_esEs5(xy30, xy400, ty_Int) → new_esEs7(xy30, xy400)
new_esEs5(xy30, xy400, ty_Float) → new_esEs6(xy30, xy400)
new_esEs5(xy30, xy400, app(ty_Maybe, bdf)) → new_esEs16(xy30, xy400, bdf)
new_esEs5(xy30, xy400, app(app(ty_Either, bdg), bdh)) → new_esEs22(xy30, xy400, bdg, bdh)
new_esEs5(xy30, xy400, app(ty_Ratio, bdc)) → new_esEs14(xy30, xy400, bdc)
new_esEs5(xy30, xy400, ty_Char) → new_esEs21(xy30, xy400)
new_esEs5(xy30, xy400, app(app(app(ty_@3, bch), bda), bdb)) → new_esEs8(xy30, xy400, bch, bda, bdb)
new_esEs8(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), bg, bh, ca) → new_asAs(new_esEs11(xy300, xy4000, bg), new_asAs(new_esEs10(xy301, xy4001, bh), new_esEs9(xy302, xy4002, ca)))
new_esEs11(xy300, xy4000, ty_Int) → new_esEs7(xy300, xy4000)
new_esEs11(xy300, xy4000, ty_@0) → new_esEs20(xy300, xy4000)
new_esEs11(xy300, xy4000, ty_Char) → new_esEs21(xy300, xy4000)
new_esEs11(xy300, xy4000, app(ty_[], eg)) → new_esEs13(xy300, xy4000, eg)
new_esEs11(xy300, xy4000, app(app(ty_@2, fd), ff)) → new_esEs15(xy300, xy4000, fd, ff)
new_esEs11(xy300, xy4000, ty_Bool) → new_esEs18(xy300, xy4000)
new_esEs11(xy300, xy4000, ty_Float) → new_esEs6(xy300, xy4000)
new_esEs11(xy300, xy4000, app(ty_Ratio, fc)) → new_esEs14(xy300, xy4000, fc)
new_esEs11(xy300, xy4000, app(app(app(ty_@3, eh), fa), fb)) → new_esEs8(xy300, xy4000, eh, fa, fb)
new_esEs11(xy300, xy4000, app(ty_Maybe, fg)) → new_esEs16(xy300, xy4000, fg)
new_esEs11(xy300, xy4000, ty_Double) → new_esEs19(xy300, xy4000)
new_esEs11(xy300, xy4000, ty_Integer) → new_esEs12(xy300, xy4000)
new_esEs11(xy300, xy4000, ty_Ordering) → new_esEs17(xy300, xy4000)
new_esEs11(xy300, xy4000, app(app(ty_Either, fh), ga)) → new_esEs22(xy300, xy4000, fh, ga)
new_esEs10(xy301, xy4001, ty_Integer) → new_esEs12(xy301, xy4001)
new_esEs10(xy301, xy4001, app(app(app(ty_@3, df), dg), dh)) → new_esEs8(xy301, xy4001, df, dg, dh)
new_esEs10(xy301, xy4001, ty_Double) → new_esEs19(xy301, xy4001)
new_esEs10(xy301, xy4001, app(ty_[], de)) → new_esEs13(xy301, xy4001, de)
new_esEs10(xy301, xy4001, ty_Int) → new_esEs7(xy301, xy4001)
new_esEs10(xy301, xy4001, app(ty_Maybe, ed)) → new_esEs16(xy301, xy4001, ed)
new_esEs10(xy301, xy4001, ty_@0) → new_esEs20(xy301, xy4001)
new_esEs10(xy301, xy4001, ty_Ordering) → new_esEs17(xy301, xy4001)
new_esEs10(xy301, xy4001, ty_Bool) → new_esEs18(xy301, xy4001)
new_esEs10(xy301, xy4001, ty_Char) → new_esEs21(xy301, xy4001)
new_esEs10(xy301, xy4001, app(ty_Ratio, ea)) → new_esEs14(xy301, xy4001, ea)
new_esEs10(xy301, xy4001, app(app(ty_Either, ee), ef)) → new_esEs22(xy301, xy4001, ee, ef)
new_esEs10(xy301, xy4001, app(app(ty_@2, eb), ec)) → new_esEs15(xy301, xy4001, eb, ec)
new_esEs10(xy301, xy4001, ty_Float) → new_esEs6(xy301, xy4001)
new_esEs9(xy302, xy4002, app(ty_[], cb)) → new_esEs13(xy302, xy4002, cb)
new_esEs9(xy302, xy4002, ty_@0) → new_esEs20(xy302, xy4002)
new_esEs9(xy302, xy4002, ty_Float) → new_esEs6(xy302, xy4002)
new_esEs9(xy302, xy4002, ty_Char) → new_esEs21(xy302, xy4002)
new_esEs9(xy302, xy4002, ty_Integer) → new_esEs12(xy302, xy4002)
new_esEs9(xy302, xy4002, app(app(ty_Either, dc), dd)) → new_esEs22(xy302, xy4002, dc, dd)
new_esEs9(xy302, xy4002, app(app(ty_@2, cg), da)) → new_esEs15(xy302, xy4002, cg, da)
new_esEs9(xy302, xy4002, ty_Bool) → new_esEs18(xy302, xy4002)
new_esEs9(xy302, xy4002, app(ty_Ratio, cf)) → new_esEs14(xy302, xy4002, cf)
new_esEs9(xy302, xy4002, ty_Ordering) → new_esEs17(xy302, xy4002)
new_esEs9(xy302, xy4002, ty_Int) → new_esEs7(xy302, xy4002)
new_esEs9(xy302, xy4002, ty_Double) → new_esEs19(xy302, xy4002)
new_esEs9(xy302, xy4002, app(app(app(ty_@3, cc), cd), ce)) → new_esEs8(xy302, xy4002, cc, cd, ce)
new_esEs9(xy302, xy4002, app(ty_Maybe, db)) → new_esEs16(xy302, xy4002, db)
new_asAs(False, xy28) → False
new_asAs(True, xy28) → xy28
new_esEs16(Just(xy300), Just(xy4000), ty_Ordering) → new_esEs17(xy300, xy4000)
new_esEs16(Just(xy300), Just(xy4000), app(app(app(ty_@3, bgf), bgg), bgh)) → new_esEs8(xy300, xy4000, bgf, bgg, bgh)
new_esEs16(Nothing, Nothing, gf) → True
new_esEs16(Just(xy300), Just(xy4000), ty_Bool) → new_esEs18(xy300, xy4000)
new_esEs22(Right(xy300), Right(xy4000), gg, app(app(ty_Either, bce), bcf)) → new_esEs22(xy300, xy4000, bce, bcf)
new_esEs22(Right(xy300), Right(xy4000), gg, app(ty_Maybe, bcd)) → new_esEs16(xy300, xy4000, bcd)
new_esEs22(Left(xy300), Left(xy4000), app(app(ty_Either, bbc), bbd), gh) → new_esEs22(xy300, xy4000, bbc, bbd)
new_esEs22(Left(xy300), Left(xy4000), app(ty_Maybe, bbb), gh) → new_esEs16(xy300, xy4000, bbb)
new_esEs16(Just(xy300), Just(xy4000), app(ty_Maybe, bhd)) → new_esEs16(xy300, xy4000, bhd)
new_esEs16(Just(xy300), Just(xy4000), app(app(ty_Either, bhe), bhf)) → new_esEs22(xy300, xy4000, bhe, bhf)
new_esEs16(Just(xy300), Just(xy4000), ty_Char) → new_esEs21(xy300, xy4000)
new_esEs16(Just(xy300), Just(xy4000), ty_Integer) → new_esEs12(xy300, xy4000)
new_esEs16(Just(xy300), Just(xy4000), app(app(ty_@2, bhb), bhc)) → new_esEs15(xy300, xy4000, bhb, bhc)
new_esEs16(Just(xy300), Just(xy4000), ty_@0) → new_esEs20(xy300, xy4000)
new_esEs16(Just(xy300), Just(xy4000), ty_Float) → new_esEs6(xy300, xy4000)
new_esEs16(Just(xy300), Just(xy4000), ty_Int) → new_esEs7(xy300, xy4000)
new_esEs16(Nothing, Just(xy4000), gf) → False
new_esEs16(Just(xy300), Nothing, gf) → False
new_esEs16(Just(xy300), Just(xy4000), app(ty_[], bge)) → new_esEs13(xy300, xy4000, bge)
new_esEs16(Just(xy300), Just(xy4000), ty_Double) → new_esEs19(xy300, xy4000)
new_esEs16(Just(xy300), Just(xy4000), app(ty_Ratio, bha)) → new_esEs14(xy300, xy4000, bha)
new_esEs14(:%(xy300, xy301), :%(xy4000, xy4001), gc) → new_asAs(new_esEs24(xy300, xy4000, gc), new_esEs23(xy301, xy4001, gc))
new_esEs24(xy300, xy4000, ty_Integer) → new_esEs12(xy300, xy4000)
new_esEs24(xy300, xy4000, ty_Int) → new_esEs7(xy300, xy4000)
new_esEs23(xy301, xy4001, ty_Int) → new_esEs7(xy301, xy4001)
new_esEs23(xy301, xy4001, ty_Integer) → new_esEs12(xy301, xy4001)
new_esEs12(Integer(xy300), Integer(xy4000)) → new_primEqInt(xy300, xy4000)
new_primEqInt(Neg(Succ(xy3000)), Pos(xy4000)) → False
new_primEqInt(Pos(Succ(xy3000)), Neg(xy4000)) → False
new_primEqInt(Neg(Zero), Pos(Succ(xy40000))) → False
new_primEqInt(Pos(Zero), Neg(Succ(xy40000))) → False
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_primEqInt(Neg(Succ(xy3000)), Neg(Succ(xy40000))) → new_primEqNat0(xy3000, xy40000)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_primEqInt(Neg(Zero), Neg(Succ(xy40000))) → False
new_primEqInt(Neg(Succ(xy3000)), Neg(Zero)) → False
new_primEqInt(Pos(Succ(xy3000)), Pos(Succ(xy40000))) → new_primEqNat0(xy3000, xy40000)
new_primEqInt(Pos(Succ(xy3000)), Pos(Zero)) → False
new_primEqInt(Pos(Zero), Pos(Succ(xy40000))) → False
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_primEqNat0(Succ(xy3000), Zero) → False
new_primEqNat0(Zero, Succ(xy40000)) → False
new_primEqNat0(Zero, Zero) → True
new_primEqNat0(Succ(xy3000), Succ(xy40000)) → new_primEqNat0(xy3000, xy40000)
new_esEs7(xy30, xy400) → new_primEqInt(xy30, xy400)
new_esEs19(Double(xy300, xy301), Double(xy4000, xy4001)) → new_esEs7(new_sr(xy300, xy4000), new_sr(xy301, xy4001))
new_sr(Pos(xy3010), Neg(xy40010)) → Neg(new_primMulNat0(xy3010, xy40010))
new_sr(Neg(xy3010), Pos(xy40010)) → Neg(new_primMulNat0(xy3010, xy40010))
new_sr(Neg(xy3010), Neg(xy40010)) → Pos(new_primMulNat0(xy3010, xy40010))
new_sr(Pos(xy3010), Pos(xy40010)) → Pos(new_primMulNat0(xy3010, xy40010))
new_primMulNat0(Zero, Zero) → Zero
new_primMulNat0(Succ(xy30100), Zero) → Zero
new_primMulNat0(Zero, Succ(xy400100)) → Zero
new_primMulNat0(Succ(xy30100), Succ(xy400100)) → new_primPlusNat0(new_primMulNat0(xy30100, Succ(xy400100)), xy400100)
new_primPlusNat0(Zero, xy400100) → Succ(xy400100)
new_primPlusNat0(Succ(xy290), xy400100) → Succ(Succ(new_primPlusNat1(xy290, xy400100)))
new_primPlusNat1(Succ(xy2900), Succ(xy4001000)) → Succ(Succ(new_primPlusNat1(xy2900, xy4001000)))
new_primPlusNat1(Zero, Succ(xy4001000)) → Succ(xy4001000)
new_primPlusNat1(Succ(xy2900), Zero) → Succ(xy2900)
new_primPlusNat1(Zero, Zero) → Zero
new_esEs13([], [], gb) → True
new_esEs13([], :(xy4000, xy4001), gb) → False
new_esEs13(:(xy300, xy301), [], gb) → False
new_esEs13(:(xy300, xy301), :(xy4000, xy4001), gb) → new_asAs(new_esEs25(xy300, xy4000, gb), new_esEs13(xy301, xy4001, gb))
new_esEs25(xy300, xy4000, ty_Ordering) → new_esEs17(xy300, xy4000)
new_esEs25(xy300, xy4000, ty_Integer) → new_esEs12(xy300, xy4000)
new_esEs25(xy300, xy4000, app(app(ty_@2, hf), hg)) → new_esEs15(xy300, xy4000, hf, hg)
new_esEs25(xy300, xy4000, ty_Int) → new_esEs7(xy300, xy4000)
new_esEs25(xy300, xy4000, app(app(ty_Either, baa), bab)) → new_esEs22(xy300, xy4000, baa, bab)
new_esEs25(xy300, xy4000, app(app(app(ty_@3, hb), hc), hd)) → new_esEs8(xy300, xy4000, hb, hc, hd)
new_esEs25(xy300, xy4000, app(ty_Ratio, he)) → new_esEs14(xy300, xy4000, he)
new_esEs25(xy300, xy4000, ty_Float) → new_esEs6(xy300, xy4000)
new_esEs25(xy300, xy4000, ty_Bool) → new_esEs18(xy300, xy4000)
new_esEs25(xy300, xy4000, app(ty_[], ha)) → new_esEs13(xy300, xy4000, ha)
new_esEs25(xy300, xy4000, ty_Char) → new_esEs21(xy300, xy4000)
new_esEs25(xy300, xy4000, ty_Double) → new_esEs19(xy300, xy4000)
new_esEs25(xy300, xy4000, app(ty_Maybe, hh)) → new_esEs16(xy300, xy4000, hh)
new_esEs25(xy300, xy4000, ty_@0) → new_esEs20(xy300, xy4000)
new_esEs20(@0, @0) → True
new_esEs21(Char(xy300), Char(xy4000)) → new_primEqNat0(xy300, xy4000)
new_esEs18(True, True) → True
new_esEs18(True, False) → False
new_esEs18(False, True) → False
new_esEs18(False, False) → True
new_esEs6(Float(xy300, xy301), Float(xy4000, xy4001)) → new_esEs7(new_sr(xy300, xy4000), new_sr(xy301, xy4001))
new_esEs22(Right(xy300), Right(xy4000), gg, ty_Ordering) → new_esEs17(xy300, xy4000)
new_esEs22(Left(xy300), Left(xy4000), ty_Float, gh) → new_esEs6(xy300, xy4000)
new_esEs22(Left(xy300), Left(xy4000), ty_Char, gh) → new_esEs21(xy300, xy4000)
new_esEs22(Right(xy300), Right(xy4000), gg, app(app(ty_@2, bcb), bcc)) → new_esEs15(xy300, xy4000, bcb, bcc)
new_esEs22(Left(xy300), Left(xy4000), ty_@0, gh) → new_esEs20(xy300, xy4000)
new_esEs22(Left(xy300), Left(xy4000), ty_Int, gh) → new_esEs7(xy300, xy4000)
new_esEs22(Left(xy300), Left(xy4000), app(app(ty_@2, bah), bba), gh) → new_esEs15(xy300, xy4000, bah, bba)
new_esEs22(Left(xy300), Left(xy4000), app(ty_[], bac), gh) → new_esEs13(xy300, xy4000, bac)
new_esEs22(Right(xy300), Right(xy4000), gg, app(app(app(ty_@3, bbf), bbg), bbh)) → new_esEs8(xy300, xy4000, bbf, bbg, bbh)
new_esEs22(Right(xy300), Right(xy4000), gg, ty_Float) → new_esEs6(xy300, xy4000)
new_esEs22(Right(xy300), Right(xy4000), gg, ty_Char) → new_esEs21(xy300, xy4000)
new_esEs22(Left(xy300), Left(xy4000), ty_Ordering, gh) → new_esEs17(xy300, xy4000)
new_esEs22(Left(xy300), Left(xy4000), ty_Integer, gh) → new_esEs12(xy300, xy4000)
new_esEs22(Left(xy300), Left(xy4000), app(ty_Ratio, bag), gh) → new_esEs14(xy300, xy4000, bag)
new_esEs22(Right(xy300), Right(xy4000), gg, ty_Int) → new_esEs7(xy300, xy4000)
new_esEs22(Right(xy300), Right(xy4000), gg, ty_Double) → new_esEs19(xy300, xy4000)
new_esEs22(Left(xy300), Left(xy4000), ty_Double, gh) → new_esEs19(xy300, xy4000)
new_esEs22(Right(xy300), Right(xy4000), gg, ty_Integer) → new_esEs12(xy300, xy4000)
new_esEs22(Right(xy300), Right(xy4000), gg, ty_Bool) → new_esEs18(xy300, xy4000)
new_esEs22(Left(xy300), Left(xy4000), app(app(app(ty_@3, bad), bae), baf), gh) → new_esEs8(xy300, xy4000, bad, bae, baf)
new_esEs22(Right(xy300), Right(xy4000), gg, app(ty_Ratio, bca)) → new_esEs14(xy300, xy4000, bca)
new_esEs22(Left(xy300), Left(xy4000), ty_Bool, gh) → new_esEs18(xy300, xy4000)
new_esEs22(Right(xy300), Left(xy4000), gg, gh) → False
new_esEs22(Left(xy300), Right(xy4000), gg, gh) → False
new_esEs22(Right(xy300), Right(xy4000), gg, ty_@0) → new_esEs20(xy300, xy4000)
new_esEs22(Right(xy300), Right(xy4000), gg, app(ty_[], bbe)) → new_esEs13(xy300, xy4000, bbe)
new_esEs17(LT, LT) → True
new_esEs17(LT, EQ) → False
new_esEs17(EQ, LT) → False
new_esEs17(EQ, EQ) → True
new_esEs17(GT, GT) → True
new_esEs17(LT, GT) → False
new_esEs17(GT, LT) → False
new_esEs17(EQ, GT) → False
new_esEs17(GT, EQ) → False
new_esEs15(@2(xy300, xy301), @2(xy4000, xy4001), gd, ge) → new_asAs(new_esEs27(xy300, xy4000, gd), new_esEs26(xy301, xy4001, ge))
new_esEs27(xy300, xy4000, app(app(ty_@2, bfh), bga)) → new_esEs15(xy300, xy4000, bfh, bga)
new_esEs27(xy300, xy4000, ty_Integer) → new_esEs12(xy300, xy4000)
new_esEs27(xy300, xy4000, app(app(ty_Either, bgc), bgd)) → new_esEs22(xy300, xy4000, bgc, bgd)
new_esEs27(xy300, xy4000, app(ty_Maybe, bgb)) → new_esEs16(xy300, xy4000, bgb)
new_esEs27(xy300, xy4000, app(ty_Ratio, bfg)) → new_esEs14(xy300, xy4000, bfg)
new_esEs27(xy300, xy4000, ty_Int) → new_esEs7(xy300, xy4000)
new_esEs27(xy300, xy4000, ty_Float) → new_esEs6(xy300, xy4000)
new_esEs27(xy300, xy4000, ty_@0) → new_esEs20(xy300, xy4000)
new_esEs27(xy300, xy4000, ty_Char) → new_esEs21(xy300, xy4000)
new_esEs27(xy300, xy4000, ty_Ordering) → new_esEs17(xy300, xy4000)
new_esEs27(xy300, xy4000, ty_Bool) → new_esEs18(xy300, xy4000)
new_esEs27(xy300, xy4000, app(ty_[], bfc)) → new_esEs13(xy300, xy4000, bfc)
new_esEs27(xy300, xy4000, app(app(app(ty_@3, bfd), bfe), bff)) → new_esEs8(xy300, xy4000, bfd, bfe, bff)
new_esEs27(xy300, xy4000, ty_Double) → new_esEs19(xy300, xy4000)
new_esEs26(xy301, xy4001, ty_Bool) → new_esEs18(xy301, xy4001)
new_esEs26(xy301, xy4001, app(app(ty_@2, bef), beg)) → new_esEs15(xy301, xy4001, bef, beg)
new_esEs26(xy301, xy4001, app(ty_Ratio, bee)) → new_esEs14(xy301, xy4001, bee)
new_esEs26(xy301, xy4001, ty_Float) → new_esEs6(xy301, xy4001)
new_esEs26(xy301, xy4001, app(app(app(ty_@3, beb), bec), bed)) → new_esEs8(xy301, xy4001, beb, bec, bed)
new_esEs26(xy301, xy4001, ty_Int) → new_esEs7(xy301, xy4001)
new_esEs26(xy301, xy4001, ty_Double) → new_esEs19(xy301, xy4001)
new_esEs26(xy301, xy4001, ty_Integer) → new_esEs12(xy301, xy4001)
new_esEs26(xy301, xy4001, app(ty_[], bea)) → new_esEs13(xy301, xy4001, bea)
new_esEs26(xy301, xy4001, ty_Ordering) → new_esEs17(xy301, xy4001)
new_esEs26(xy301, xy4001, app(app(ty_Either, bfa), bfb)) → new_esEs22(xy301, xy4001, bfa, bfb)
new_esEs26(xy301, xy4001, app(ty_Maybe, beh)) → new_esEs16(xy301, xy4001, beh)
new_esEs26(xy301, xy4001, ty_@0) → new_esEs20(xy301, xy4001)
new_esEs26(xy301, xy4001, ty_Char) → new_esEs21(xy301, xy4001)

The set Q consists of the following terms:

new_esEs10(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs17(LT, GT)
new_esEs17(GT, LT)
new_esEs27(x0, x1, app(app(ty_@2, x2), x3))
new_esEs27(x0, x1, app(ty_[], x2))
new_esEs12(Integer(x0), Integer(x1))
new_esEs11(x0, x1, ty_Bool)
new_esEs5(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs22(Right(x0), Right(x1), x2, ty_@0)
new_esEs16(Just(x0), Just(x1), app(ty_Maybe, x2))
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_esEs27(x0, x1, ty_@0)
new_esEs22(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs22(Right(x0), Right(x1), x2, ty_Int)
new_esEs17(LT, LT)
new_esEs27(x0, x1, ty_Float)
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_esEs16(Just(x0), Just(x1), ty_Ordering)
new_esEs14(:%(x0, x1), :%(x2, x3), x4)
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs9(x0, x1, ty_Int)
new_esEs10(x0, x1, ty_Ordering)
new_esEs18(False, True)
new_esEs18(True, False)
new_asAs(False, x0)
new_esEs10(x0, x1, app(app(ty_Either, x2), x3))
new_primPlusNat1(Succ(x0), Zero)
new_esEs9(x0, x1, ty_Bool)
new_esEs5(x0, x1, ty_Bool)
new_esEs25(x0, x1, ty_Double)
new_esEs16(Just(x0), Just(x1), app(ty_[], x2))
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs5(x0, x1, app(ty_Ratio, x2))
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs23(x0, x1, ty_Integer)
new_esEs7(x0, x1)
new_esEs9(x0, x1, ty_Integer)
new_esEs22(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs11(x0, x1, ty_Ordering)
new_esEs13([], [], x0)
new_esEs9(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs17(EQ, GT)
new_esEs17(GT, EQ)
new_esEs22(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs22(Left(x0), Left(x1), ty_Double, x2)
new_esEs9(x0, x1, app(app(ty_@2, x2), x3))
new_esEs11(x0, x1, ty_Float)
new_esEs9(x0, x1, app(ty_Ratio, x2))
new_esEs11(x0, x1, app(app(ty_@2, x2), x3))
new_esEs22(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs27(x0, x1, ty_Integer)
new_esEs5(x0, x1, app(ty_Maybe, x2))
new_esEs27(x0, x1, ty_Ordering)
new_esEs18(True, True)
new_esEs26(x0, x1, ty_Double)
new_esEs26(x0, x1, ty_Integer)
new_primPlusNat1(Zero, Succ(x0))
new_esEs16(Just(x0), Just(x1), ty_Double)
new_primPlusNat0(Zero, x0)
new_esEs25(x0, x1, ty_Float)
new_esEs26(x0, x1, ty_Int)
new_esEs10(x0, x1, app(ty_Maybe, x2))
new_esEs16(Nothing, Nothing, x0)
new_esEs8(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_asAs(True, x0)
new_esEs25(x0, x1, ty_Bool)
new_esEs16(Just(x0), Just(x1), ty_Float)
new_esEs5(x0, x1, app(ty_[], x2))
new_esEs17(GT, GT)
new_esEs25(x0, x1, ty_Int)
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_esEs11(x0, x1, ty_Int)
new_esEs27(x0, x1, ty_Int)
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs25(x0, x1, ty_Integer)
new_esEs9(x0, x1, ty_Double)
new_esEs22(Right(x0), Right(x1), x2, ty_Bool)
new_esEs26(x0, x1, ty_Bool)
new_esEs25(x0, x1, ty_Char)
new_sr(Pos(x0), Pos(x1))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs22(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs10(x0, x1, app(app(ty_@2, x2), x3))
new_primEqNat0(Zero, Zero)
new_esEs24(x0, x1, ty_Int)
new_esEs24(x0, x1, ty_Integer)
new_esEs22(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs9(x0, x1, ty_Char)
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs22(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs16(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs22(Right(x0), Right(x1), x2, ty_Float)
new_primEqNat0(Zero, Succ(x0))
new_esEs10(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_Int)
new_esEs22(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs10(x0, x1, ty_Char)
new_esEs6(Float(x0, x1), Float(x2, x3))
new_esEs27(x0, x1, app(ty_Ratio, x2))
new_esEs11(x0, x1, app(app(ty_Either, x2), x3))
new_esEs13(:(x0, x1), [], x2)
new_esEs22(Left(x0), Left(x1), ty_@0, x2)
new_esEs5(x0, x1, ty_Double)
new_esEs9(x0, x1, ty_@0)
new_primMulNat0(Zero, Zero)
new_esEs25(x0, x1, ty_@0)
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs19(Double(x0, x1), Double(x2, x3))
new_esEs22(Left(x0), Left(x1), ty_Bool, x2)
new_esEs22(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs9(x0, x1, ty_Float)
new_esEs26(x0, x1, ty_Char)
new_esEs9(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs5(x0, x1, ty_@0)
new_esEs16(Just(x0), Just(x1), ty_@0)
new_esEs9(x0, x1, ty_Ordering)
new_esEs13([], :(x0, x1), x2)
new_esEs10(x0, x1, ty_Float)
new_esEs27(x0, x1, app(ty_Maybe, x2))
new_esEs5(x0, x1, app(app(ty_Either, x2), x3))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs22(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs11(x0, x1, app(ty_[], x2))
new_esEs16(Nothing, Just(x0), x1)
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_esEs9(x0, x1, app(ty_Maybe, x2))
new_esEs26(x0, x1, app(ty_[], x2))
new_esEs10(x0, x1, app(ty_Ratio, x2))
new_esEs27(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, ty_Ordering)
new_esEs22(Left(x0), Left(x1), ty_Integer, x2)
new_esEs16(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_esEs21(Char(x0), Char(x1))
new_esEs15(@2(x0, x1), @2(x2, x3), x4, x5)
new_primMulNat0(Zero, Succ(x0))
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs11(x0, x1, ty_Char)
new_esEs22(Right(x0), Right(x1), x2, ty_Integer)
new_esEs27(x0, x1, ty_Char)
new_esEs11(x0, x1, ty_@0)
new_esEs5(x0, x1, app(app(ty_@2, x2), x3))
new_esEs16(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs22(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs22(Left(x0), Left(x1), ty_Char, x2)
new_esEs16(Just(x0), Just(x1), ty_Integer)
new_esEs10(x0, x1, ty_Integer)
new_esEs18(False, False)
new_esEs27(x0, x1, ty_Double)
new_esEs20(@0, @0)
new_esEs16(Just(x0), Just(x1), ty_Int)
new_esEs22(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs22(Right(x0), Right(x1), x2, ty_Char)
new_esEs11(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs26(x0, x1, ty_@0)
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs22(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs13(:(x0, x1), :(x2, x3), x4)
new_esEs11(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs10(x0, x1, ty_Bool)
new_primEqNat0(Succ(x0), Zero)
new_sr(Neg(x0), Neg(x1))
new_esEs10(x0, x1, ty_Double)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_esEs5(x0, x1, ty_Integer)
new_primPlusNat1(Zero, Zero)
new_esEs5(x0, x1, ty_Ordering)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs27(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(Left(x0), Left(x1), ty_Int, x2)
new_esEs16(Just(x0), Nothing, x1)
new_esEs5(x0, x1, ty_Char)
new_esEs22(Left(x0), Right(x1), x2, x3)
new_esEs22(Right(x0), Left(x1), x2, x3)
new_primEqInt(Pos(Zero), Pos(Zero))
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs11(x0, x1, app(ty_Maybe, x2))
new_primPlusNat0(Succ(x0), x1)
new_esEs26(x0, x1, ty_Ordering)
new_esEs5(x0, x1, ty_Float)
new_esEs22(Right(x0), Right(x1), x2, ty_Double)
new_esEs17(EQ, EQ)
new_esEs17(EQ, LT)
new_esEs17(LT, EQ)
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs11(x0, x1, ty_Double)
new_esEs16(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs22(Left(x0), Left(x1), ty_Float, x2)
new_esEs10(x0, x1, ty_Int)
new_esEs16(Just(x0), Just(x1), ty_Bool)
new_esEs5(x0, x1, ty_Int)
new_esEs9(x0, x1, app(ty_[], x2))
new_esEs26(x0, x1, ty_Float)
new_esEs27(x0, x1, ty_Bool)
new_primMulNat0(Succ(x0), Zero)
new_esEs10(x0, x1, app(ty_[], x2))
new_esEs11(x0, x1, ty_Integer)
new_esEs16(Just(x0), Just(x1), ty_Char)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ IFR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ DependencyGraphProof
                      ↳ AND
                        ↳ QDP
QDP
                          ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

new_deleteBy0(xy10, xy11, xy12, False, ba, bb) → new_deleteBy(Left(xy12), xy10, ba, bb)
new_deleteBy(Left(xy30), :(Left(xy400), xy41), bc, bd) → new_deleteBy0(xy41, xy400, xy30, new_esEs4(xy30, xy400, bc), bc, bd)
new_deleteBy(Left(xy30), :(Right(xy400), xy41), bc, bd) → new_deleteBy(Left(xy30), xy41, bc, bd)

The TRS R consists of the following rules:

new_esEs10(xy301, xy4001, ty_Integer) → new_esEs12(xy301, xy4001)
new_esEs25(xy300, xy4000, ty_Ordering) → new_esEs17(xy300, xy4000)
new_esEs9(xy302, xy4002, app(ty_[], cb)) → new_esEs13(xy302, xy4002, cb)
new_esEs5(xy30, xy400, ty_Double) → new_esEs19(xy30, xy400)
new_primPlusNat1(Succ(xy2900), Succ(xy4001000)) → Succ(Succ(new_primPlusNat1(xy2900, xy4001000)))
new_esEs25(xy300, xy4000, ty_Integer) → new_esEs12(xy300, xy4000)
new_esEs26(xy301, xy4001, ty_Bool) → new_esEs18(xy301, xy4001)
new_esEs22(Left(xy300), Left(xy4000), app(ty_Maybe, bbb), gh) → new_esEs16(xy300, xy4000, bbb)
new_primEqInt(Neg(Succ(xy3000)), Pos(xy4000)) → False
new_primEqInt(Pos(Succ(xy3000)), Neg(xy4000)) → False
new_esEs10(xy301, xy4001, app(app(app(ty_@3, df), dg), dh)) → new_esEs8(xy301, xy4001, df, dg, dh)
new_esEs22(Right(xy300), Right(xy4000), gg, ty_Ordering) → new_esEs17(xy300, xy4000)
new_esEs9(xy302, xy4002, ty_@0) → new_esEs20(xy302, xy4002)
new_esEs5(xy30, xy400, app(app(ty_@2, bdd), bde)) → new_esEs15(xy30, xy400, bdd, bde)
new_esEs5(xy30, xy400, ty_Integer) → new_esEs12(xy30, xy400)
new_esEs22(Left(xy300), Left(xy4000), ty_Float, gh) → new_esEs6(xy300, xy4000)
new_esEs13([], [], gb) → True
new_esEs22(Left(xy300), Left(xy4000), ty_Char, gh) → new_esEs21(xy300, xy4000)
new_esEs9(xy302, xy4002, ty_Float) → new_esEs6(xy302, xy4002)
new_primEqInt(Neg(Zero), Pos(Succ(xy40000))) → False
new_primEqInt(Pos(Zero), Neg(Succ(xy40000))) → False
new_esEs10(xy301, xy4001, ty_Double) → new_esEs19(xy301, xy4001)
new_esEs22(Right(xy300), Right(xy4000), gg, app(app(ty_@2, bcb), bcc)) → new_esEs15(xy300, xy4000, bcb, bcc)
new_esEs16(Just(xy300), Just(xy4000), ty_Ordering) → new_esEs17(xy300, xy4000)
new_esEs26(xy301, xy4001, app(app(ty_@2, bef), beg)) → new_esEs15(xy301, xy4001, bef, beg)
new_esEs16(Just(xy300), Just(xy4000), app(app(app(ty_@3, bgf), bgg), bgh)) → new_esEs8(xy300, xy4000, bgf, bgg, bgh)
new_primMulNat0(Zero, Zero) → Zero
new_esEs16(Nothing, Nothing, gf) → True
new_esEs11(xy300, xy4000, ty_Int) → new_esEs7(xy300, xy4000)
new_esEs11(xy300, xy4000, ty_@0) → new_esEs20(xy300, xy4000)
new_esEs4(xy30, xy400, ty_Int) → new_esEs7(xy30, xy400)
new_esEs4(xy30, xy400, ty_Char) → new_esEs21(xy30, xy400)
new_primPlusNat0(Zero, xy400100) → Succ(xy400100)
new_esEs26(xy301, xy4001, app(ty_Ratio, bee)) → new_esEs14(xy301, xy4001, bee)
new_esEs27(xy300, xy4000, app(app(ty_@2, bfh), bga)) → new_esEs15(xy300, xy4000, bfh, bga)
new_esEs22(Left(xy300), Left(xy4000), ty_@0, gh) → new_esEs20(xy300, xy4000)
new_esEs25(xy300, xy4000, app(app(ty_@2, hf), hg)) → new_esEs15(xy300, xy4000, hf, hg)
new_esEs27(xy300, xy4000, ty_Integer) → new_esEs12(xy300, xy4000)
new_esEs25(xy300, xy4000, ty_Int) → new_esEs7(xy300, xy4000)
new_esEs23(xy301, xy4001, ty_Int) → new_esEs7(xy301, xy4001)
new_esEs22(Left(xy300), Left(xy4000), app(app(ty_Either, bbc), bbd), gh) → new_esEs22(xy300, xy4000, bbc, bbd)
new_esEs22(Left(xy300), Left(xy4000), ty_Int, gh) → new_esEs7(xy300, xy4000)
new_esEs11(xy300, xy4000, ty_Char) → new_esEs21(xy300, xy4000)
new_esEs26(xy301, xy4001, ty_Float) → new_esEs6(xy301, xy4001)
new_esEs24(xy300, xy4000, ty_Integer) → new_esEs12(xy300, xy4000)
new_sr(Pos(xy3010), Neg(xy40010)) → Neg(new_primMulNat0(xy3010, xy40010))
new_sr(Neg(xy3010), Pos(xy40010)) → Neg(new_primMulNat0(xy3010, xy40010))
new_esEs16(Just(xy300), Just(xy4000), ty_Bool) → new_esEs18(xy300, xy4000)
new_esEs11(xy300, xy4000, app(ty_[], eg)) → new_esEs13(xy300, xy4000, eg)
new_esEs4(xy30, xy400, ty_@0) → new_esEs20(xy30, xy400)
new_esEs16(Just(xy300), Just(xy4000), app(ty_Maybe, bhd)) → new_esEs16(xy300, xy4000, bhd)
new_esEs4(xy30, xy400, ty_Float) → new_esEs6(xy30, xy400)
new_esEs11(xy300, xy4000, app(app(ty_@2, fd), ff)) → new_esEs15(xy300, xy4000, fd, ff)
new_esEs8(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), bg, bh, ca) → new_asAs(new_esEs11(xy300, xy4000, bg), new_asAs(new_esEs10(xy301, xy4001, bh), new_esEs9(xy302, xy4002, ca)))
new_esEs4(xy30, xy400, ty_Double) → new_esEs19(xy30, xy400)
new_esEs22(Right(xy300), Right(xy4000), gg, app(ty_Maybe, bcd)) → new_esEs16(xy300, xy4000, bcd)
new_esEs26(xy301, xy4001, app(app(app(ty_@3, beb), bec), bed)) → new_esEs8(xy301, xy4001, beb, bec, bed)
new_esEs16(Just(xy300), Just(xy4000), ty_Char) → new_esEs21(xy300, xy4000)
new_esEs9(xy302, xy4002, ty_Char) → new_esEs21(xy302, xy4002)
new_esEs23(xy301, xy4001, ty_Integer) → new_esEs12(xy301, xy4001)
new_esEs12(Integer(xy300), Integer(xy4000)) → new_primEqInt(xy300, xy4000)
new_esEs11(xy300, xy4000, ty_Bool) → new_esEs18(xy300, xy4000)
new_esEs27(xy300, xy4000, app(app(ty_Either, bgc), bgd)) → new_esEs22(xy300, xy4000, bgc, bgd)
new_esEs25(xy300, xy4000, app(app(ty_Either, baa), bab)) → new_esEs22(xy300, xy4000, baa, bab)
new_primEqNat0(Succ(xy3000), Zero) → False
new_primEqNat0(Zero, Succ(xy40000)) → False
new_esEs4(xy30, xy400, app(ty_Ratio, gc)) → new_esEs14(xy30, xy400, gc)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs10(xy301, xy4001, app(ty_[], de)) → new_esEs13(xy301, xy4001, de)
new_esEs20(@0, @0) → True
new_esEs5(xy30, xy400, ty_Ordering) → new_esEs17(xy30, xy400)
new_esEs22(Left(xy300), Left(xy4000), app(app(ty_@2, bah), bba), gh) → new_esEs15(xy300, xy4000, bah, bba)
new_esEs11(xy300, xy4000, ty_Float) → new_esEs6(xy300, xy4000)
new_esEs5(xy30, xy400, app(ty_[], bcg)) → new_esEs13(xy30, xy400, bcg)
new_esEs22(Left(xy300), Left(xy4000), app(ty_[], bac), gh) → new_esEs13(xy300, xy4000, bac)
new_esEs25(xy300, xy4000, app(app(app(ty_@3, hb), hc), hd)) → new_esEs8(xy300, xy4000, hb, hc, hd)
new_esEs10(xy301, xy4001, ty_Int) → new_esEs7(xy301, xy4001)
new_esEs5(xy30, xy400, ty_Bool) → new_esEs18(xy30, xy400)
new_esEs9(xy302, xy4002, ty_Integer) → new_esEs12(xy302, xy4002)
new_esEs9(xy302, xy4002, app(app(ty_Either, dc), dd)) → new_esEs22(xy302, xy4002, dc, dd)
new_esEs9(xy302, xy4002, app(app(ty_@2, cg), da)) → new_esEs15(xy302, xy4002, cg, da)
new_esEs9(xy302, xy4002, ty_Bool) → new_esEs18(xy302, xy4002)
new_esEs27(xy300, xy4000, app(ty_Maybe, bgb)) → new_esEs16(xy300, xy4000, bgb)
new_esEs24(xy300, xy4000, ty_Int) → new_esEs7(xy300, xy4000)
new_esEs5(xy30, xy400, ty_@0) → new_esEs20(xy30, xy400)
new_esEs22(Right(xy300), Right(xy4000), gg, app(app(app(ty_@3, bbf), bbg), bbh)) → new_esEs8(xy300, xy4000, bbf, bbg, bbh)
new_esEs25(xy300, xy4000, app(ty_Ratio, he)) → new_esEs14(xy300, xy4000, he)
new_esEs4(xy30, xy400, app(app(ty_Either, gg), gh)) → new_esEs22(xy30, xy400, gg, gh)
new_esEs22(Right(xy300), Right(xy4000), gg, ty_Float) → new_esEs6(xy300, xy4000)
new_esEs22(Right(xy300), Right(xy4000), gg, ty_Char) → new_esEs21(xy300, xy4000)
new_esEs16(Just(xy300), Just(xy4000), ty_Integer) → new_esEs12(xy300, xy4000)
new_esEs6(Float(xy300, xy301), Float(xy4000, xy4001)) → new_esEs7(new_sr(xy300, xy4000), new_sr(xy301, xy4001))
new_esEs10(xy301, xy4001, app(ty_Maybe, ed)) → new_esEs16(xy301, xy4001, ed)
new_esEs11(xy300, xy4000, app(ty_Ratio, fc)) → new_esEs14(xy300, xy4000, fc)
new_esEs17(LT, LT) → True
new_esEs27(xy300, xy4000, app(ty_Ratio, bfg)) → new_esEs14(xy300, xy4000, bfg)
new_esEs22(Left(xy300), Left(xy4000), ty_Ordering, gh) → new_esEs17(xy300, xy4000)
new_esEs22(Left(xy300), Left(xy4000), ty_Integer, gh) → new_esEs12(xy300, xy4000)
new_esEs25(xy300, xy4000, ty_Float) → new_esEs6(xy300, xy4000)
new_esEs16(Just(xy300), Just(xy4000), app(app(ty_@2, bhb), bhc)) → new_esEs15(xy300, xy4000, bhb, bhc)
new_esEs9(xy302, xy4002, app(ty_Ratio, cf)) → new_esEs14(xy302, xy4002, cf)
new_sr(Neg(xy3010), Neg(xy40010)) → Pos(new_primMulNat0(xy3010, xy40010))
new_esEs9(xy302, xy4002, ty_Ordering) → new_esEs17(xy302, xy4002)
new_esEs27(xy300, xy4000, ty_Int) → new_esEs7(xy300, xy4000)
new_esEs11(xy300, xy4000, app(app(app(ty_@3, eh), fa), fb)) → new_esEs8(xy300, xy4000, eh, fa, fb)
new_esEs5(xy30, xy400, ty_Int) → new_esEs7(xy30, xy400)
new_asAs(False, xy28) → False
new_sr(Pos(xy3010), Pos(xy40010)) → Pos(new_primMulNat0(xy3010, xy40010))
new_primEqNat0(Zero, Zero) → True
new_esEs4(xy30, xy400, app(app(ty_@2, gd), ge)) → new_esEs15(xy30, xy400, gd, ge)
new_esEs13([], :(xy4000, xy4001), gb) → False
new_esEs13(:(xy300, xy301), [], gb) → False
new_primMulNat0(Succ(xy30100), Zero) → Zero
new_primMulNat0(Zero, Succ(xy400100)) → Zero
new_esEs13(:(xy300, xy301), :(xy4000, xy4001), gb) → new_asAs(new_esEs25(xy300, xy4000, gb), new_esEs13(xy301, xy4001, gb))
new_esEs25(xy300, xy4000, ty_Bool) → new_esEs18(xy300, xy4000)
new_esEs18(True, True) → True
new_esEs7(xy30, xy400) → new_primEqInt(xy30, xy400)
new_esEs16(Just(xy300), Just(xy4000), ty_@0) → new_esEs20(xy300, xy4000)
new_esEs10(xy301, xy4001, ty_@0) → new_esEs20(xy301, xy4001)
new_esEs27(xy300, xy4000, ty_Float) → new_esEs6(xy300, xy4000)
new_esEs5(xy30, xy400, ty_Float) → new_esEs6(xy30, xy400)
new_esEs4(xy30, xy400, ty_Integer) → new_esEs12(xy30, xy400)
new_esEs22(Left(xy300), Left(xy4000), app(ty_Ratio, bag), gh) → new_esEs14(xy300, xy4000, bag)
new_esEs26(xy301, xy4001, ty_Int) → new_esEs7(xy301, xy4001)
new_esEs16(Just(xy300), Just(xy4000), ty_Float) → new_esEs6(xy300, xy4000)
new_esEs27(xy300, xy4000, ty_@0) → new_esEs20(xy300, xy4000)
new_primPlusNat0(Succ(xy290), xy400100) → Succ(Succ(new_primPlusNat1(xy290, xy400100)))
new_esEs25(xy300, xy4000, app(ty_[], ha)) → new_esEs13(xy300, xy4000, ha)
new_esEs11(xy300, xy4000, app(ty_Maybe, fg)) → new_esEs16(xy300, xy4000, fg)
new_esEs10(xy301, xy4001, ty_Ordering) → new_esEs17(xy301, xy4001)
new_esEs5(xy30, xy400, app(ty_Maybe, bdf)) → new_esEs16(xy30, xy400, bdf)
new_esEs17(LT, EQ) → False
new_esEs17(EQ, LT) → False
new_esEs26(xy301, xy4001, ty_Double) → new_esEs19(xy301, xy4001)
new_esEs10(xy301, xy4001, ty_Bool) → new_esEs18(xy301, xy4001)
new_esEs21(Char(xy300), Char(xy4000)) → new_primEqNat0(xy300, xy4000)
new_esEs25(xy300, xy4000, ty_Char) → new_esEs21(xy300, xy4000)
new_esEs4(xy30, xy400, ty_Bool) → new_esEs18(xy30, xy400)
new_esEs26(xy301, xy4001, ty_Integer) → new_esEs12(xy301, xy4001)
new_primEqInt(Neg(Succ(xy3000)), Neg(Succ(xy40000))) → new_primEqNat0(xy3000, xy40000)
new_esEs11(xy300, xy4000, ty_Double) → new_esEs19(xy300, xy4000)
new_esEs16(Just(xy300), Just(xy4000), ty_Int) → new_esEs7(xy300, xy4000)
new_esEs10(xy301, xy4001, ty_Char) → new_esEs21(xy301, xy4001)
new_esEs26(xy301, xy4001, app(ty_[], bea)) → new_esEs13(xy301, xy4001, bea)
new_esEs27(xy300, xy4000, ty_Char) → new_esEs21(xy300, xy4000)
new_primPlusNat1(Zero, Succ(xy4001000)) → Succ(xy4001000)
new_primPlusNat1(Succ(xy2900), Zero) → Succ(xy2900)
new_esEs11(xy300, xy4000, ty_Integer) → new_esEs12(xy300, xy4000)
new_esEs16(Just(xy300), Just(xy4000), app(app(ty_Either, bhe), bhf)) → new_esEs22(xy300, xy4000, bhe, bhf)
new_esEs9(xy302, xy4002, ty_Int) → new_esEs7(xy302, xy4002)
new_esEs26(xy301, xy4001, ty_Ordering) → new_esEs17(xy301, xy4001)
new_esEs26(xy301, xy4001, app(app(ty_Either, bfa), bfb)) → new_esEs22(xy301, xy4001, bfa, bfb)
new_esEs22(Right(xy300), Right(xy4000), gg, ty_Int) → new_esEs7(xy300, xy4000)
new_esEs22(Right(xy300), Right(xy4000), gg, ty_Double) → new_esEs19(xy300, xy4000)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs27(xy300, xy4000, ty_Ordering) → new_esEs17(xy300, xy4000)
new_esEs17(EQ, EQ) → True
new_esEs19(Double(xy300, xy301), Double(xy4000, xy4001)) → new_esEs7(new_sr(xy300, xy4000), new_sr(xy301, xy4001))
new_esEs18(True, False) → False
new_esEs18(False, True) → False
new_esEs16(Nothing, Just(xy4000), gf) → False
new_esEs16(Just(xy300), Nothing, gf) → False
new_primEqInt(Neg(Zero), Neg(Succ(xy40000))) → False
new_primEqInt(Neg(Succ(xy3000)), Neg(Zero)) → False
new_esEs27(xy300, xy4000, ty_Bool) → new_esEs18(xy300, xy4000)
new_esEs26(xy301, xy4001, app(ty_Maybe, beh)) → new_esEs16(xy301, xy4001, beh)
new_esEs10(xy301, xy4001, app(ty_Ratio, ea)) → new_esEs14(xy301, xy4001, ea)
new_esEs25(xy300, xy4000, ty_Double) → new_esEs19(xy300, xy4000)
new_esEs25(xy300, xy4000, app(ty_Maybe, hh)) → new_esEs16(xy300, xy4000, hh)
new_esEs16(Just(xy300), Just(xy4000), app(ty_[], bge)) → new_esEs13(xy300, xy4000, bge)
new_esEs22(Left(xy300), Left(xy4000), ty_Double, gh) → new_esEs19(xy300, xy4000)
new_primPlusNat1(Zero, Zero) → Zero
new_esEs22(Right(xy300), Right(xy4000), gg, ty_Integer) → new_esEs12(xy300, xy4000)
new_asAs(True, xy28) → xy28
new_esEs22(Right(xy300), Right(xy4000), gg, ty_Bool) → new_esEs18(xy300, xy4000)
new_esEs16(Just(xy300), Just(xy4000), ty_Double) → new_esEs19(xy300, xy4000)
new_esEs22(Left(xy300), Left(xy4000), app(app(app(ty_@3, bad), bae), baf), gh) → new_esEs8(xy300, xy4000, bad, bae, baf)
new_primMulNat0(Succ(xy30100), Succ(xy400100)) → new_primPlusNat0(new_primMulNat0(xy30100, Succ(xy400100)), xy400100)
new_esEs27(xy300, xy4000, app(ty_[], bfc)) → new_esEs13(xy300, xy4000, bfc)
new_esEs9(xy302, xy4002, ty_Double) → new_esEs19(xy302, xy4002)
new_esEs9(xy302, xy4002, app(app(app(ty_@3, cc), cd), ce)) → new_esEs8(xy302, xy4002, cc, cd, ce)
new_esEs22(Right(xy300), Right(xy4000), gg, app(ty_Ratio, bca)) → new_esEs14(xy300, xy4000, bca)
new_esEs17(GT, GT) → True
new_esEs14(:%(xy300, xy301), :%(xy4000, xy4001), gc) → new_asAs(new_esEs24(xy300, xy4000, gc), new_esEs23(xy301, xy4001, gc))
new_primEqInt(Pos(Succ(xy3000)), Pos(Succ(xy40000))) → new_primEqNat0(xy3000, xy40000)
new_esEs4(xy30, xy400, app(ty_[], gb)) → new_esEs13(xy30, xy400, gb)
new_esEs11(xy300, xy4000, ty_Ordering) → new_esEs17(xy300, xy4000)
new_esEs22(Left(xy300), Left(xy4000), ty_Bool, gh) → new_esEs18(xy300, xy4000)
new_esEs10(xy301, xy4001, app(app(ty_Either, ee), ef)) → new_esEs22(xy301, xy4001, ee, ef)
new_esEs22(Right(xy300), Left(xy4000), gg, gh) → False
new_esEs22(Left(xy300), Right(xy4000), gg, gh) → False
new_esEs5(xy30, xy400, app(app(ty_Either, bdg), bdh)) → new_esEs22(xy30, xy400, bdg, bdh)
new_esEs17(LT, GT) → False
new_esEs17(GT, LT) → False
new_primEqNat0(Succ(xy3000), Succ(xy40000)) → new_primEqNat0(xy3000, xy40000)
new_esEs4(xy30, xy400, app(ty_Maybe, gf)) → new_esEs16(xy30, xy400, gf)
new_esEs17(EQ, GT) → False
new_esEs17(GT, EQ) → False
new_esEs27(xy300, xy4000, app(app(app(ty_@3, bfd), bfe), bff)) → new_esEs8(xy300, xy4000, bfd, bfe, bff)
new_esEs22(Right(xy300), Right(xy4000), gg, ty_@0) → new_esEs20(xy300, xy4000)
new_esEs26(xy301, xy4001, ty_@0) → new_esEs20(xy301, xy4001)
new_esEs10(xy301, xy4001, app(app(ty_@2, eb), ec)) → new_esEs15(xy301, xy4001, eb, ec)
new_esEs11(xy300, xy4000, app(app(ty_Either, fh), ga)) → new_esEs22(xy300, xy4000, fh, ga)
new_esEs9(xy302, xy4002, app(ty_Maybe, db)) → new_esEs16(xy302, xy4002, db)
new_esEs25(xy300, xy4000, ty_@0) → new_esEs20(xy300, xy4000)
new_esEs16(Just(xy300), Just(xy4000), app(ty_Ratio, bha)) → new_esEs14(xy300, xy4000, bha)
new_esEs10(xy301, xy4001, ty_Float) → new_esEs6(xy301, xy4001)
new_esEs5(xy30, xy400, app(ty_Ratio, bdc)) → new_esEs14(xy30, xy400, bdc)
new_esEs4(xy30, xy400, ty_Ordering) → new_esEs17(xy30, xy400)
new_esEs5(xy30, xy400, ty_Char) → new_esEs21(xy30, xy400)
new_esEs5(xy30, xy400, app(app(app(ty_@3, bch), bda), bdb)) → new_esEs8(xy30, xy400, bch, bda, bdb)
new_primEqInt(Pos(Succ(xy3000)), Pos(Zero)) → False
new_primEqInt(Pos(Zero), Pos(Succ(xy40000))) → False
new_esEs26(xy301, xy4001, ty_Char) → new_esEs21(xy301, xy4001)
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_esEs22(Right(xy300), Right(xy4000), gg, app(app(ty_Either, bce), bcf)) → new_esEs22(xy300, xy4000, bce, bcf)
new_esEs4(xy30, xy400, app(app(app(ty_@3, bg), bh), ca)) → new_esEs8(xy30, xy400, bg, bh, ca)
new_esEs15(@2(xy300, xy301), @2(xy4000, xy4001), gd, ge) → new_asAs(new_esEs27(xy300, xy4000, gd), new_esEs26(xy301, xy4001, ge))
new_esEs22(Right(xy300), Right(xy4000), gg, app(ty_[], bbe)) → new_esEs13(xy300, xy4000, bbe)
new_esEs18(False, False) → True
new_esEs27(xy300, xy4000, ty_Double) → new_esEs19(xy300, xy4000)

The set Q consists of the following terms:

new_esEs10(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs17(LT, GT)
new_esEs17(GT, LT)
new_esEs27(x0, x1, app(app(ty_@2, x2), x3))
new_esEs4(x0, x1, app(ty_[], x2))
new_esEs27(x0, x1, app(ty_[], x2))
new_esEs12(Integer(x0), Integer(x1))
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs11(x0, x1, ty_Bool)
new_esEs5(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs22(Right(x0), Right(x1), x2, ty_@0)
new_esEs4(x0, x1, ty_Bool)
new_esEs16(Just(x0), Just(x1), app(ty_Maybe, x2))
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_esEs27(x0, x1, ty_@0)
new_esEs22(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs22(Right(x0), Right(x1), x2, ty_Int)
new_esEs17(LT, LT)
new_esEs27(x0, x1, ty_Float)
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_esEs16(Just(x0), Just(x1), ty_Ordering)
new_esEs14(:%(x0, x1), :%(x2, x3), x4)
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs9(x0, x1, ty_Int)
new_esEs4(x0, x1, ty_Double)
new_esEs10(x0, x1, ty_Ordering)
new_esEs18(False, True)
new_esEs18(True, False)
new_asAs(False, x0)
new_esEs10(x0, x1, app(app(ty_Either, x2), x3))
new_primPlusNat1(Succ(x0), Zero)
new_esEs9(x0, x1, ty_Bool)
new_esEs5(x0, x1, ty_Bool)
new_esEs25(x0, x1, ty_Double)
new_esEs16(Just(x0), Just(x1), app(ty_[], x2))
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs5(x0, x1, app(ty_Ratio, x2))
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs4(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_Integer)
new_esEs7(x0, x1)
new_esEs9(x0, x1, ty_Integer)
new_esEs22(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs11(x0, x1, ty_Ordering)
new_esEs13([], [], x0)
new_esEs9(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs17(EQ, GT)
new_esEs17(GT, EQ)
new_esEs22(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs22(Left(x0), Left(x1), ty_Double, x2)
new_esEs9(x0, x1, app(app(ty_@2, x2), x3))
new_esEs11(x0, x1, ty_Float)
new_esEs9(x0, x1, app(ty_Ratio, x2))
new_esEs11(x0, x1, app(app(ty_@2, x2), x3))
new_esEs22(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs27(x0, x1, ty_Integer)
new_esEs5(x0, x1, app(ty_Maybe, x2))
new_esEs27(x0, x1, ty_Ordering)
new_esEs18(True, True)
new_esEs26(x0, x1, ty_Double)
new_esEs26(x0, x1, ty_Integer)
new_primPlusNat1(Zero, Succ(x0))
new_esEs16(Just(x0), Just(x1), ty_Double)
new_primPlusNat0(Zero, x0)
new_esEs25(x0, x1, ty_Float)
new_esEs26(x0, x1, ty_Int)
new_esEs10(x0, x1, app(ty_Maybe, x2))
new_esEs16(Nothing, Nothing, x0)
new_esEs8(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_asAs(True, x0)
new_esEs25(x0, x1, ty_Bool)
new_esEs16(Just(x0), Just(x1), ty_Float)
new_esEs5(x0, x1, app(ty_[], x2))
new_esEs17(GT, GT)
new_esEs25(x0, x1, ty_Int)
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_esEs4(x0, x1, ty_Char)
new_esEs11(x0, x1, ty_Int)
new_esEs27(x0, x1, ty_Int)
new_esEs4(x0, x1, ty_Integer)
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs25(x0, x1, ty_Integer)
new_esEs9(x0, x1, ty_Double)
new_esEs22(Right(x0), Right(x1), x2, ty_Bool)
new_esEs26(x0, x1, ty_Bool)
new_esEs25(x0, x1, ty_Char)
new_sr(Pos(x0), Pos(x1))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs22(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs10(x0, x1, app(app(ty_@2, x2), x3))
new_primEqNat0(Zero, Zero)
new_esEs24(x0, x1, ty_Int)
new_esEs24(x0, x1, ty_Integer)
new_esEs22(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs4(x0, x1, ty_Float)
new_esEs9(x0, x1, ty_Char)
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs22(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs16(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs22(Right(x0), Right(x1), x2, ty_Float)
new_primEqNat0(Zero, Succ(x0))
new_esEs10(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_Int)
new_esEs22(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs10(x0, x1, ty_Char)
new_esEs6(Float(x0, x1), Float(x2, x3))
new_esEs27(x0, x1, app(ty_Ratio, x2))
new_esEs11(x0, x1, app(app(ty_Either, x2), x3))
new_esEs13(:(x0, x1), [], x2)
new_esEs22(Left(x0), Left(x1), ty_@0, x2)
new_esEs5(x0, x1, ty_Double)
new_esEs9(x0, x1, ty_@0)
new_primMulNat0(Zero, Zero)
new_esEs25(x0, x1, ty_@0)
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs19(Double(x0, x1), Double(x2, x3))
new_esEs22(Left(x0), Left(x1), ty_Bool, x2)
new_esEs22(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs9(x0, x1, ty_Float)
new_esEs26(x0, x1, ty_Char)
new_esEs9(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs5(x0, x1, ty_@0)
new_esEs16(Just(x0), Just(x1), ty_@0)
new_esEs9(x0, x1, ty_Ordering)
new_esEs13([], :(x0, x1), x2)
new_esEs10(x0, x1, ty_Float)
new_esEs27(x0, x1, app(ty_Maybe, x2))
new_esEs5(x0, x1, app(app(ty_Either, x2), x3))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs22(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs11(x0, x1, app(ty_[], x2))
new_esEs16(Nothing, Just(x0), x1)
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_esEs9(x0, x1, app(ty_Maybe, x2))
new_esEs26(x0, x1, app(ty_[], x2))
new_esEs10(x0, x1, app(ty_Ratio, x2))
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs27(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, ty_Ordering)
new_esEs22(Left(x0), Left(x1), ty_Integer, x2)
new_esEs16(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_esEs21(Char(x0), Char(x1))
new_esEs15(@2(x0, x1), @2(x2, x3), x4, x5)
new_primMulNat0(Zero, Succ(x0))
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs11(x0, x1, ty_Char)
new_esEs22(Right(x0), Right(x1), x2, ty_Integer)
new_esEs27(x0, x1, ty_Char)
new_esEs11(x0, x1, ty_@0)
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs5(x0, x1, app(app(ty_@2, x2), x3))
new_esEs16(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs22(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs22(Left(x0), Left(x1), ty_Char, x2)
new_esEs16(Just(x0), Just(x1), ty_Integer)
new_esEs10(x0, x1, ty_Integer)
new_esEs18(False, False)
new_esEs27(x0, x1, ty_Double)
new_esEs20(@0, @0)
new_esEs16(Just(x0), Just(x1), ty_Int)
new_esEs22(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs4(x0, x1, ty_Ordering)
new_esEs22(Right(x0), Right(x1), x2, ty_Char)
new_esEs11(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs26(x0, x1, ty_@0)
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs22(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs13(:(x0, x1), :(x2, x3), x4)
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs11(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs10(x0, x1, ty_Bool)
new_primEqNat0(Succ(x0), Zero)
new_sr(Neg(x0), Neg(x1))
new_esEs10(x0, x1, ty_Double)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_esEs5(x0, x1, ty_Integer)
new_primPlusNat1(Zero, Zero)
new_esEs5(x0, x1, ty_Ordering)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs27(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(Left(x0), Left(x1), ty_Int, x2)
new_esEs4(x0, x1, ty_Int)
new_esEs16(Just(x0), Nothing, x1)
new_esEs5(x0, x1, ty_Char)
new_esEs22(Left(x0), Right(x1), x2, x3)
new_esEs22(Right(x0), Left(x1), x2, x3)
new_primEqInt(Pos(Zero), Pos(Zero))
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs11(x0, x1, app(ty_Maybe, x2))
new_primPlusNat0(Succ(x0), x1)
new_esEs26(x0, x1, ty_Ordering)
new_esEs5(x0, x1, ty_Float)
new_esEs22(Right(x0), Right(x1), x2, ty_Double)
new_esEs17(EQ, EQ)
new_esEs17(EQ, LT)
new_esEs17(LT, EQ)
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs11(x0, x1, ty_Double)
new_esEs16(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs22(Left(x0), Left(x1), ty_Float, x2)
new_esEs10(x0, x1, ty_Int)
new_esEs16(Just(x0), Just(x1), ty_Bool)
new_esEs5(x0, x1, ty_Int)
new_esEs9(x0, x1, app(ty_[], x2))
new_esEs26(x0, x1, ty_Float)
new_esEs27(x0, x1, ty_Bool)
new_primMulNat0(Succ(x0), Zero)
new_esEs10(x0, x1, app(ty_[], x2))
new_esEs11(x0, x1, ty_Integer)
new_esEs16(Just(x0), Just(x1), ty_Char)

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL
  ↳ IFR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ DependencyGraphProof
                      ↳ AND
                        ↳ QDP
                        ↳ QDP
                          ↳ UsableRulesProof
QDP
                              ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

new_deleteBy0(xy10, xy11, xy12, False, ba, bb) → new_deleteBy(Left(xy12), xy10, ba, bb)
new_deleteBy(Left(xy30), :(Left(xy400), xy41), bc, bd) → new_deleteBy0(xy41, xy400, xy30, new_esEs4(xy30, xy400, bc), bc, bd)
new_deleteBy(Left(xy30), :(Right(xy400), xy41), bc, bd) → new_deleteBy(Left(xy30), xy41, bc, bd)

The TRS R consists of the following rules:

new_esEs4(xy30, xy400, ty_Int) → new_esEs7(xy30, xy400)
new_esEs4(xy30, xy400, ty_Char) → new_esEs21(xy30, xy400)
new_esEs4(xy30, xy400, ty_@0) → new_esEs20(xy30, xy400)
new_esEs4(xy30, xy400, ty_Float) → new_esEs6(xy30, xy400)
new_esEs4(xy30, xy400, ty_Double) → new_esEs19(xy30, xy400)
new_esEs4(xy30, xy400, app(ty_Ratio, gc)) → new_esEs14(xy30, xy400, gc)
new_esEs4(xy30, xy400, app(app(ty_Either, gg), gh)) → new_esEs22(xy30, xy400, gg, gh)
new_esEs4(xy30, xy400, app(app(ty_@2, gd), ge)) → new_esEs15(xy30, xy400, gd, ge)
new_esEs4(xy30, xy400, ty_Integer) → new_esEs12(xy30, xy400)
new_esEs4(xy30, xy400, ty_Bool) → new_esEs18(xy30, xy400)
new_esEs4(xy30, xy400, app(ty_[], gb)) → new_esEs13(xy30, xy400, gb)
new_esEs4(xy30, xy400, app(ty_Maybe, gf)) → new_esEs16(xy30, xy400, gf)
new_esEs4(xy30, xy400, ty_Ordering) → new_esEs17(xy30, xy400)
new_esEs4(xy30, xy400, app(app(app(ty_@3, bg), bh), ca)) → new_esEs8(xy30, xy400, bg, bh, ca)
new_esEs8(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), bg, bh, ca) → new_asAs(new_esEs11(xy300, xy4000, bg), new_asAs(new_esEs10(xy301, xy4001, bh), new_esEs9(xy302, xy4002, ca)))
new_esEs11(xy300, xy4000, ty_Int) → new_esEs7(xy300, xy4000)
new_esEs11(xy300, xy4000, ty_@0) → new_esEs20(xy300, xy4000)
new_esEs11(xy300, xy4000, ty_Char) → new_esEs21(xy300, xy4000)
new_esEs11(xy300, xy4000, app(ty_[], eg)) → new_esEs13(xy300, xy4000, eg)
new_esEs11(xy300, xy4000, app(app(ty_@2, fd), ff)) → new_esEs15(xy300, xy4000, fd, ff)
new_esEs11(xy300, xy4000, ty_Bool) → new_esEs18(xy300, xy4000)
new_esEs11(xy300, xy4000, ty_Float) → new_esEs6(xy300, xy4000)
new_esEs11(xy300, xy4000, app(ty_Ratio, fc)) → new_esEs14(xy300, xy4000, fc)
new_esEs11(xy300, xy4000, app(app(app(ty_@3, eh), fa), fb)) → new_esEs8(xy300, xy4000, eh, fa, fb)
new_esEs11(xy300, xy4000, app(ty_Maybe, fg)) → new_esEs16(xy300, xy4000, fg)
new_esEs11(xy300, xy4000, ty_Double) → new_esEs19(xy300, xy4000)
new_esEs11(xy300, xy4000, ty_Integer) → new_esEs12(xy300, xy4000)
new_esEs11(xy300, xy4000, ty_Ordering) → new_esEs17(xy300, xy4000)
new_esEs11(xy300, xy4000, app(app(ty_Either, fh), ga)) → new_esEs22(xy300, xy4000, fh, ga)
new_esEs10(xy301, xy4001, ty_Integer) → new_esEs12(xy301, xy4001)
new_esEs10(xy301, xy4001, app(app(app(ty_@3, df), dg), dh)) → new_esEs8(xy301, xy4001, df, dg, dh)
new_esEs10(xy301, xy4001, ty_Double) → new_esEs19(xy301, xy4001)
new_esEs10(xy301, xy4001, app(ty_[], de)) → new_esEs13(xy301, xy4001, de)
new_esEs10(xy301, xy4001, ty_Int) → new_esEs7(xy301, xy4001)
new_esEs10(xy301, xy4001, app(ty_Maybe, ed)) → new_esEs16(xy301, xy4001, ed)
new_esEs10(xy301, xy4001, ty_@0) → new_esEs20(xy301, xy4001)
new_esEs10(xy301, xy4001, ty_Ordering) → new_esEs17(xy301, xy4001)
new_esEs10(xy301, xy4001, ty_Bool) → new_esEs18(xy301, xy4001)
new_esEs10(xy301, xy4001, ty_Char) → new_esEs21(xy301, xy4001)
new_esEs10(xy301, xy4001, app(ty_Ratio, ea)) → new_esEs14(xy301, xy4001, ea)
new_esEs10(xy301, xy4001, app(app(ty_Either, ee), ef)) → new_esEs22(xy301, xy4001, ee, ef)
new_esEs10(xy301, xy4001, app(app(ty_@2, eb), ec)) → new_esEs15(xy301, xy4001, eb, ec)
new_esEs10(xy301, xy4001, ty_Float) → new_esEs6(xy301, xy4001)
new_esEs9(xy302, xy4002, app(ty_[], cb)) → new_esEs13(xy302, xy4002, cb)
new_esEs9(xy302, xy4002, ty_@0) → new_esEs20(xy302, xy4002)
new_esEs9(xy302, xy4002, ty_Float) → new_esEs6(xy302, xy4002)
new_esEs9(xy302, xy4002, ty_Char) → new_esEs21(xy302, xy4002)
new_esEs9(xy302, xy4002, ty_Integer) → new_esEs12(xy302, xy4002)
new_esEs9(xy302, xy4002, app(app(ty_Either, dc), dd)) → new_esEs22(xy302, xy4002, dc, dd)
new_esEs9(xy302, xy4002, app(app(ty_@2, cg), da)) → new_esEs15(xy302, xy4002, cg, da)
new_esEs9(xy302, xy4002, ty_Bool) → new_esEs18(xy302, xy4002)
new_esEs9(xy302, xy4002, app(ty_Ratio, cf)) → new_esEs14(xy302, xy4002, cf)
new_esEs9(xy302, xy4002, ty_Ordering) → new_esEs17(xy302, xy4002)
new_esEs9(xy302, xy4002, ty_Int) → new_esEs7(xy302, xy4002)
new_esEs9(xy302, xy4002, ty_Double) → new_esEs19(xy302, xy4002)
new_esEs9(xy302, xy4002, app(app(app(ty_@3, cc), cd), ce)) → new_esEs8(xy302, xy4002, cc, cd, ce)
new_esEs9(xy302, xy4002, app(ty_Maybe, db)) → new_esEs16(xy302, xy4002, db)
new_asAs(False, xy28) → False
new_asAs(True, xy28) → xy28
new_esEs16(Just(xy300), Just(xy4000), ty_Ordering) → new_esEs17(xy300, xy4000)
new_esEs16(Just(xy300), Just(xy4000), app(app(app(ty_@3, bgf), bgg), bgh)) → new_esEs8(xy300, xy4000, bgf, bgg, bgh)
new_esEs16(Nothing, Nothing, gf) → True
new_esEs16(Just(xy300), Just(xy4000), ty_Bool) → new_esEs18(xy300, xy4000)
new_esEs22(Right(xy300), Right(xy4000), gg, app(app(ty_Either, bce), bcf)) → new_esEs22(xy300, xy4000, bce, bcf)
new_esEs22(Right(xy300), Right(xy4000), gg, app(ty_Maybe, bcd)) → new_esEs16(xy300, xy4000, bcd)
new_esEs22(Left(xy300), Left(xy4000), app(app(ty_Either, bbc), bbd), gh) → new_esEs22(xy300, xy4000, bbc, bbd)
new_esEs22(Left(xy300), Left(xy4000), app(ty_Maybe, bbb), gh) → new_esEs16(xy300, xy4000, bbb)
new_esEs16(Just(xy300), Just(xy4000), app(ty_Maybe, bhd)) → new_esEs16(xy300, xy4000, bhd)
new_esEs16(Just(xy300), Just(xy4000), app(app(ty_Either, bhe), bhf)) → new_esEs22(xy300, xy4000, bhe, bhf)
new_esEs16(Just(xy300), Just(xy4000), ty_Char) → new_esEs21(xy300, xy4000)
new_esEs16(Just(xy300), Just(xy4000), ty_Integer) → new_esEs12(xy300, xy4000)
new_esEs16(Just(xy300), Just(xy4000), app(app(ty_@2, bhb), bhc)) → new_esEs15(xy300, xy4000, bhb, bhc)
new_esEs16(Just(xy300), Just(xy4000), ty_@0) → new_esEs20(xy300, xy4000)
new_esEs16(Just(xy300), Just(xy4000), ty_Float) → new_esEs6(xy300, xy4000)
new_esEs16(Just(xy300), Just(xy4000), ty_Int) → new_esEs7(xy300, xy4000)
new_esEs16(Nothing, Just(xy4000), gf) → False
new_esEs16(Just(xy300), Nothing, gf) → False
new_esEs16(Just(xy300), Just(xy4000), app(ty_[], bge)) → new_esEs13(xy300, xy4000, bge)
new_esEs16(Just(xy300), Just(xy4000), ty_Double) → new_esEs19(xy300, xy4000)
new_esEs16(Just(xy300), Just(xy4000), app(ty_Ratio, bha)) → new_esEs14(xy300, xy4000, bha)
new_esEs14(:%(xy300, xy301), :%(xy4000, xy4001), gc) → new_asAs(new_esEs24(xy300, xy4000, gc), new_esEs23(xy301, xy4001, gc))
new_esEs24(xy300, xy4000, ty_Integer) → new_esEs12(xy300, xy4000)
new_esEs24(xy300, xy4000, ty_Int) → new_esEs7(xy300, xy4000)
new_esEs23(xy301, xy4001, ty_Int) → new_esEs7(xy301, xy4001)
new_esEs23(xy301, xy4001, ty_Integer) → new_esEs12(xy301, xy4001)
new_esEs12(Integer(xy300), Integer(xy4000)) → new_primEqInt(xy300, xy4000)
new_primEqInt(Neg(Succ(xy3000)), Pos(xy4000)) → False
new_primEqInt(Pos(Succ(xy3000)), Neg(xy4000)) → False
new_primEqInt(Neg(Zero), Pos(Succ(xy40000))) → False
new_primEqInt(Pos(Zero), Neg(Succ(xy40000))) → False
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_primEqInt(Neg(Succ(xy3000)), Neg(Succ(xy40000))) → new_primEqNat0(xy3000, xy40000)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_primEqInt(Neg(Zero), Neg(Succ(xy40000))) → False
new_primEqInt(Neg(Succ(xy3000)), Neg(Zero)) → False
new_primEqInt(Pos(Succ(xy3000)), Pos(Succ(xy40000))) → new_primEqNat0(xy3000, xy40000)
new_primEqInt(Pos(Succ(xy3000)), Pos(Zero)) → False
new_primEqInt(Pos(Zero), Pos(Succ(xy40000))) → False
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_primEqNat0(Succ(xy3000), Zero) → False
new_primEqNat0(Zero, Succ(xy40000)) → False
new_primEqNat0(Zero, Zero) → True
new_primEqNat0(Succ(xy3000), Succ(xy40000)) → new_primEqNat0(xy3000, xy40000)
new_esEs7(xy30, xy400) → new_primEqInt(xy30, xy400)
new_esEs19(Double(xy300, xy301), Double(xy4000, xy4001)) → new_esEs7(new_sr(xy300, xy4000), new_sr(xy301, xy4001))
new_sr(Pos(xy3010), Neg(xy40010)) → Neg(new_primMulNat0(xy3010, xy40010))
new_sr(Neg(xy3010), Pos(xy40010)) → Neg(new_primMulNat0(xy3010, xy40010))
new_sr(Neg(xy3010), Neg(xy40010)) → Pos(new_primMulNat0(xy3010, xy40010))
new_sr(Pos(xy3010), Pos(xy40010)) → Pos(new_primMulNat0(xy3010, xy40010))
new_primMulNat0(Zero, Zero) → Zero
new_primMulNat0(Succ(xy30100), Zero) → Zero
new_primMulNat0(Zero, Succ(xy400100)) → Zero
new_primMulNat0(Succ(xy30100), Succ(xy400100)) → new_primPlusNat0(new_primMulNat0(xy30100, Succ(xy400100)), xy400100)
new_primPlusNat0(Zero, xy400100) → Succ(xy400100)
new_primPlusNat0(Succ(xy290), xy400100) → Succ(Succ(new_primPlusNat1(xy290, xy400100)))
new_primPlusNat1(Succ(xy2900), Succ(xy4001000)) → Succ(Succ(new_primPlusNat1(xy2900, xy4001000)))
new_primPlusNat1(Zero, Succ(xy4001000)) → Succ(xy4001000)
new_primPlusNat1(Succ(xy2900), Zero) → Succ(xy2900)
new_primPlusNat1(Zero, Zero) → Zero
new_esEs13([], [], gb) → True
new_esEs13([], :(xy4000, xy4001), gb) → False
new_esEs13(:(xy300, xy301), [], gb) → False
new_esEs13(:(xy300, xy301), :(xy4000, xy4001), gb) → new_asAs(new_esEs25(xy300, xy4000, gb), new_esEs13(xy301, xy4001, gb))
new_esEs25(xy300, xy4000, ty_Ordering) → new_esEs17(xy300, xy4000)
new_esEs25(xy300, xy4000, ty_Integer) → new_esEs12(xy300, xy4000)
new_esEs25(xy300, xy4000, app(app(ty_@2, hf), hg)) → new_esEs15(xy300, xy4000, hf, hg)
new_esEs25(xy300, xy4000, ty_Int) → new_esEs7(xy300, xy4000)
new_esEs25(xy300, xy4000, app(app(ty_Either, baa), bab)) → new_esEs22(xy300, xy4000, baa, bab)
new_esEs25(xy300, xy4000, app(app(app(ty_@3, hb), hc), hd)) → new_esEs8(xy300, xy4000, hb, hc, hd)
new_esEs25(xy300, xy4000, app(ty_Ratio, he)) → new_esEs14(xy300, xy4000, he)
new_esEs25(xy300, xy4000, ty_Float) → new_esEs6(xy300, xy4000)
new_esEs25(xy300, xy4000, ty_Bool) → new_esEs18(xy300, xy4000)
new_esEs25(xy300, xy4000, app(ty_[], ha)) → new_esEs13(xy300, xy4000, ha)
new_esEs25(xy300, xy4000, ty_Char) → new_esEs21(xy300, xy4000)
new_esEs25(xy300, xy4000, ty_Double) → new_esEs19(xy300, xy4000)
new_esEs25(xy300, xy4000, app(ty_Maybe, hh)) → new_esEs16(xy300, xy4000, hh)
new_esEs25(xy300, xy4000, ty_@0) → new_esEs20(xy300, xy4000)
new_esEs20(@0, @0) → True
new_esEs21(Char(xy300), Char(xy4000)) → new_primEqNat0(xy300, xy4000)
new_esEs18(True, True) → True
new_esEs18(True, False) → False
new_esEs18(False, True) → False
new_esEs18(False, False) → True
new_esEs6(Float(xy300, xy301), Float(xy4000, xy4001)) → new_esEs7(new_sr(xy300, xy4000), new_sr(xy301, xy4001))
new_esEs22(Right(xy300), Right(xy4000), gg, ty_Ordering) → new_esEs17(xy300, xy4000)
new_esEs22(Left(xy300), Left(xy4000), ty_Float, gh) → new_esEs6(xy300, xy4000)
new_esEs22(Left(xy300), Left(xy4000), ty_Char, gh) → new_esEs21(xy300, xy4000)
new_esEs22(Right(xy300), Right(xy4000), gg, app(app(ty_@2, bcb), bcc)) → new_esEs15(xy300, xy4000, bcb, bcc)
new_esEs22(Left(xy300), Left(xy4000), ty_@0, gh) → new_esEs20(xy300, xy4000)
new_esEs22(Left(xy300), Left(xy4000), ty_Int, gh) → new_esEs7(xy300, xy4000)
new_esEs22(Left(xy300), Left(xy4000), app(app(ty_@2, bah), bba), gh) → new_esEs15(xy300, xy4000, bah, bba)
new_esEs22(Left(xy300), Left(xy4000), app(ty_[], bac), gh) → new_esEs13(xy300, xy4000, bac)
new_esEs22(Right(xy300), Right(xy4000), gg, app(app(app(ty_@3, bbf), bbg), bbh)) → new_esEs8(xy300, xy4000, bbf, bbg, bbh)
new_esEs22(Right(xy300), Right(xy4000), gg, ty_Float) → new_esEs6(xy300, xy4000)
new_esEs22(Right(xy300), Right(xy4000), gg, ty_Char) → new_esEs21(xy300, xy4000)
new_esEs22(Left(xy300), Left(xy4000), ty_Ordering, gh) → new_esEs17(xy300, xy4000)
new_esEs22(Left(xy300), Left(xy4000), ty_Integer, gh) → new_esEs12(xy300, xy4000)
new_esEs22(Left(xy300), Left(xy4000), app(ty_Ratio, bag), gh) → new_esEs14(xy300, xy4000, bag)
new_esEs22(Right(xy300), Right(xy4000), gg, ty_Int) → new_esEs7(xy300, xy4000)
new_esEs22(Right(xy300), Right(xy4000), gg, ty_Double) → new_esEs19(xy300, xy4000)
new_esEs22(Left(xy300), Left(xy4000), ty_Double, gh) → new_esEs19(xy300, xy4000)
new_esEs22(Right(xy300), Right(xy4000), gg, ty_Integer) → new_esEs12(xy300, xy4000)
new_esEs22(Right(xy300), Right(xy4000), gg, ty_Bool) → new_esEs18(xy300, xy4000)
new_esEs22(Left(xy300), Left(xy4000), app(app(app(ty_@3, bad), bae), baf), gh) → new_esEs8(xy300, xy4000, bad, bae, baf)
new_esEs22(Right(xy300), Right(xy4000), gg, app(ty_Ratio, bca)) → new_esEs14(xy300, xy4000, bca)
new_esEs22(Left(xy300), Left(xy4000), ty_Bool, gh) → new_esEs18(xy300, xy4000)
new_esEs22(Right(xy300), Left(xy4000), gg, gh) → False
new_esEs22(Left(xy300), Right(xy4000), gg, gh) → False
new_esEs22(Right(xy300), Right(xy4000), gg, ty_@0) → new_esEs20(xy300, xy4000)
new_esEs22(Right(xy300), Right(xy4000), gg, app(ty_[], bbe)) → new_esEs13(xy300, xy4000, bbe)
new_esEs17(LT, LT) → True
new_esEs17(LT, EQ) → False
new_esEs17(EQ, LT) → False
new_esEs17(EQ, EQ) → True
new_esEs17(GT, GT) → True
new_esEs17(LT, GT) → False
new_esEs17(GT, LT) → False
new_esEs17(EQ, GT) → False
new_esEs17(GT, EQ) → False
new_esEs15(@2(xy300, xy301), @2(xy4000, xy4001), gd, ge) → new_asAs(new_esEs27(xy300, xy4000, gd), new_esEs26(xy301, xy4001, ge))
new_esEs27(xy300, xy4000, app(app(ty_@2, bfh), bga)) → new_esEs15(xy300, xy4000, bfh, bga)
new_esEs27(xy300, xy4000, ty_Integer) → new_esEs12(xy300, xy4000)
new_esEs27(xy300, xy4000, app(app(ty_Either, bgc), bgd)) → new_esEs22(xy300, xy4000, bgc, bgd)
new_esEs27(xy300, xy4000, app(ty_Maybe, bgb)) → new_esEs16(xy300, xy4000, bgb)
new_esEs27(xy300, xy4000, app(ty_Ratio, bfg)) → new_esEs14(xy300, xy4000, bfg)
new_esEs27(xy300, xy4000, ty_Int) → new_esEs7(xy300, xy4000)
new_esEs27(xy300, xy4000, ty_Float) → new_esEs6(xy300, xy4000)
new_esEs27(xy300, xy4000, ty_@0) → new_esEs20(xy300, xy4000)
new_esEs27(xy300, xy4000, ty_Char) → new_esEs21(xy300, xy4000)
new_esEs27(xy300, xy4000, ty_Ordering) → new_esEs17(xy300, xy4000)
new_esEs27(xy300, xy4000, ty_Bool) → new_esEs18(xy300, xy4000)
new_esEs27(xy300, xy4000, app(ty_[], bfc)) → new_esEs13(xy300, xy4000, bfc)
new_esEs27(xy300, xy4000, app(app(app(ty_@3, bfd), bfe), bff)) → new_esEs8(xy300, xy4000, bfd, bfe, bff)
new_esEs27(xy300, xy4000, ty_Double) → new_esEs19(xy300, xy4000)
new_esEs26(xy301, xy4001, ty_Bool) → new_esEs18(xy301, xy4001)
new_esEs26(xy301, xy4001, app(app(ty_@2, bef), beg)) → new_esEs15(xy301, xy4001, bef, beg)
new_esEs26(xy301, xy4001, app(ty_Ratio, bee)) → new_esEs14(xy301, xy4001, bee)
new_esEs26(xy301, xy4001, ty_Float) → new_esEs6(xy301, xy4001)
new_esEs26(xy301, xy4001, app(app(app(ty_@3, beb), bec), bed)) → new_esEs8(xy301, xy4001, beb, bec, bed)
new_esEs26(xy301, xy4001, ty_Int) → new_esEs7(xy301, xy4001)
new_esEs26(xy301, xy4001, ty_Double) → new_esEs19(xy301, xy4001)
new_esEs26(xy301, xy4001, ty_Integer) → new_esEs12(xy301, xy4001)
new_esEs26(xy301, xy4001, app(ty_[], bea)) → new_esEs13(xy301, xy4001, bea)
new_esEs26(xy301, xy4001, ty_Ordering) → new_esEs17(xy301, xy4001)
new_esEs26(xy301, xy4001, app(app(ty_Either, bfa), bfb)) → new_esEs22(xy301, xy4001, bfa, bfb)
new_esEs26(xy301, xy4001, app(ty_Maybe, beh)) → new_esEs16(xy301, xy4001, beh)
new_esEs26(xy301, xy4001, ty_@0) → new_esEs20(xy301, xy4001)
new_esEs26(xy301, xy4001, ty_Char) → new_esEs21(xy301, xy4001)

The set Q consists of the following terms:

new_esEs10(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs17(LT, GT)
new_esEs17(GT, LT)
new_esEs27(x0, x1, app(app(ty_@2, x2), x3))
new_esEs4(x0, x1, app(ty_[], x2))
new_esEs27(x0, x1, app(ty_[], x2))
new_esEs12(Integer(x0), Integer(x1))
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs11(x0, x1, ty_Bool)
new_esEs5(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs22(Right(x0), Right(x1), x2, ty_@0)
new_esEs4(x0, x1, ty_Bool)
new_esEs16(Just(x0), Just(x1), app(ty_Maybe, x2))
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_esEs27(x0, x1, ty_@0)
new_esEs22(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs22(Right(x0), Right(x1), x2, ty_Int)
new_esEs17(LT, LT)
new_esEs27(x0, x1, ty_Float)
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_esEs16(Just(x0), Just(x1), ty_Ordering)
new_esEs14(:%(x0, x1), :%(x2, x3), x4)
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs9(x0, x1, ty_Int)
new_esEs4(x0, x1, ty_Double)
new_esEs10(x0, x1, ty_Ordering)
new_esEs18(False, True)
new_esEs18(True, False)
new_asAs(False, x0)
new_esEs10(x0, x1, app(app(ty_Either, x2), x3))
new_primPlusNat1(Succ(x0), Zero)
new_esEs9(x0, x1, ty_Bool)
new_esEs5(x0, x1, ty_Bool)
new_esEs25(x0, x1, ty_Double)
new_esEs16(Just(x0), Just(x1), app(ty_[], x2))
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs5(x0, x1, app(ty_Ratio, x2))
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs4(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_Integer)
new_esEs7(x0, x1)
new_esEs9(x0, x1, ty_Integer)
new_esEs22(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs11(x0, x1, ty_Ordering)
new_esEs13([], [], x0)
new_esEs9(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs17(EQ, GT)
new_esEs17(GT, EQ)
new_esEs22(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs22(Left(x0), Left(x1), ty_Double, x2)
new_esEs9(x0, x1, app(app(ty_@2, x2), x3))
new_esEs11(x0, x1, ty_Float)
new_esEs9(x0, x1, app(ty_Ratio, x2))
new_esEs11(x0, x1, app(app(ty_@2, x2), x3))
new_esEs22(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs27(x0, x1, ty_Integer)
new_esEs5(x0, x1, app(ty_Maybe, x2))
new_esEs27(x0, x1, ty_Ordering)
new_esEs18(True, True)
new_esEs26(x0, x1, ty_Double)
new_esEs26(x0, x1, ty_Integer)
new_primPlusNat1(Zero, Succ(x0))
new_esEs16(Just(x0), Just(x1), ty_Double)
new_primPlusNat0(Zero, x0)
new_esEs25(x0, x1, ty_Float)
new_esEs26(x0, x1, ty_Int)
new_esEs10(x0, x1, app(ty_Maybe, x2))
new_esEs16(Nothing, Nothing, x0)
new_esEs8(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_asAs(True, x0)
new_esEs25(x0, x1, ty_Bool)
new_esEs16(Just(x0), Just(x1), ty_Float)
new_esEs5(x0, x1, app(ty_[], x2))
new_esEs17(GT, GT)
new_esEs25(x0, x1, ty_Int)
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_esEs4(x0, x1, ty_Char)
new_esEs11(x0, x1, ty_Int)
new_esEs27(x0, x1, ty_Int)
new_esEs4(x0, x1, ty_Integer)
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs25(x0, x1, ty_Integer)
new_esEs9(x0, x1, ty_Double)
new_esEs22(Right(x0), Right(x1), x2, ty_Bool)
new_esEs26(x0, x1, ty_Bool)
new_esEs25(x0, x1, ty_Char)
new_sr(Pos(x0), Pos(x1))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs22(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs10(x0, x1, app(app(ty_@2, x2), x3))
new_primEqNat0(Zero, Zero)
new_esEs24(x0, x1, ty_Int)
new_esEs24(x0, x1, ty_Integer)
new_esEs22(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs4(x0, x1, ty_Float)
new_esEs9(x0, x1, ty_Char)
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs22(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs16(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs22(Right(x0), Right(x1), x2, ty_Float)
new_primEqNat0(Zero, Succ(x0))
new_esEs10(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_Int)
new_esEs22(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs10(x0, x1, ty_Char)
new_esEs6(Float(x0, x1), Float(x2, x3))
new_esEs27(x0, x1, app(ty_Ratio, x2))
new_esEs11(x0, x1, app(app(ty_Either, x2), x3))
new_esEs13(:(x0, x1), [], x2)
new_esEs22(Left(x0), Left(x1), ty_@0, x2)
new_esEs5(x0, x1, ty_Double)
new_esEs9(x0, x1, ty_@0)
new_primMulNat0(Zero, Zero)
new_esEs25(x0, x1, ty_@0)
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs19(Double(x0, x1), Double(x2, x3))
new_esEs22(Left(x0), Left(x1), ty_Bool, x2)
new_esEs22(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs9(x0, x1, ty_Float)
new_esEs26(x0, x1, ty_Char)
new_esEs9(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs5(x0, x1, ty_@0)
new_esEs16(Just(x0), Just(x1), ty_@0)
new_esEs9(x0, x1, ty_Ordering)
new_esEs13([], :(x0, x1), x2)
new_esEs10(x0, x1, ty_Float)
new_esEs27(x0, x1, app(ty_Maybe, x2))
new_esEs5(x0, x1, app(app(ty_Either, x2), x3))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs22(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs11(x0, x1, app(ty_[], x2))
new_esEs16(Nothing, Just(x0), x1)
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_esEs9(x0, x1, app(ty_Maybe, x2))
new_esEs26(x0, x1, app(ty_[], x2))
new_esEs10(x0, x1, app(ty_Ratio, x2))
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs27(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, ty_Ordering)
new_esEs22(Left(x0), Left(x1), ty_Integer, x2)
new_esEs16(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_esEs21(Char(x0), Char(x1))
new_esEs15(@2(x0, x1), @2(x2, x3), x4, x5)
new_primMulNat0(Zero, Succ(x0))
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs11(x0, x1, ty_Char)
new_esEs22(Right(x0), Right(x1), x2, ty_Integer)
new_esEs27(x0, x1, ty_Char)
new_esEs11(x0, x1, ty_@0)
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs5(x0, x1, app(app(ty_@2, x2), x3))
new_esEs16(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs22(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs22(Left(x0), Left(x1), ty_Char, x2)
new_esEs16(Just(x0), Just(x1), ty_Integer)
new_esEs10(x0, x1, ty_Integer)
new_esEs18(False, False)
new_esEs27(x0, x1, ty_Double)
new_esEs20(@0, @0)
new_esEs16(Just(x0), Just(x1), ty_Int)
new_esEs22(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs4(x0, x1, ty_Ordering)
new_esEs22(Right(x0), Right(x1), x2, ty_Char)
new_esEs11(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs26(x0, x1, ty_@0)
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs22(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs13(:(x0, x1), :(x2, x3), x4)
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs11(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs10(x0, x1, ty_Bool)
new_primEqNat0(Succ(x0), Zero)
new_sr(Neg(x0), Neg(x1))
new_esEs10(x0, x1, ty_Double)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_esEs5(x0, x1, ty_Integer)
new_primPlusNat1(Zero, Zero)
new_esEs5(x0, x1, ty_Ordering)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs27(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(Left(x0), Left(x1), ty_Int, x2)
new_esEs4(x0, x1, ty_Int)
new_esEs16(Just(x0), Nothing, x1)
new_esEs5(x0, x1, ty_Char)
new_esEs22(Left(x0), Right(x1), x2, x3)
new_esEs22(Right(x0), Left(x1), x2, x3)
new_primEqInt(Pos(Zero), Pos(Zero))
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs11(x0, x1, app(ty_Maybe, x2))
new_primPlusNat0(Succ(x0), x1)
new_esEs26(x0, x1, ty_Ordering)
new_esEs5(x0, x1, ty_Float)
new_esEs22(Right(x0), Right(x1), x2, ty_Double)
new_esEs17(EQ, EQ)
new_esEs17(EQ, LT)
new_esEs17(LT, EQ)
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs11(x0, x1, ty_Double)
new_esEs16(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs22(Left(x0), Left(x1), ty_Float, x2)
new_esEs10(x0, x1, ty_Int)
new_esEs16(Just(x0), Just(x1), ty_Bool)
new_esEs5(x0, x1, ty_Int)
new_esEs9(x0, x1, app(ty_[], x2))
new_esEs26(x0, x1, ty_Float)
new_esEs27(x0, x1, ty_Bool)
new_primMulNat0(Succ(x0), Zero)
new_esEs10(x0, x1, app(ty_[], x2))
new_esEs11(x0, x1, ty_Integer)
new_esEs16(Just(x0), Just(x1), ty_Char)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_esEs5(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs5(x0, x1, ty_Bool)
new_esEs5(x0, x1, app(ty_Ratio, x2))
new_esEs5(x0, x1, app(ty_Maybe, x2))
new_esEs5(x0, x1, app(ty_[], x2))
new_esEs5(x0, x1, ty_Double)
new_esEs5(x0, x1, ty_@0)
new_esEs5(x0, x1, app(app(ty_Either, x2), x3))
new_esEs5(x0, x1, app(app(ty_@2, x2), x3))
new_esEs5(x0, x1, ty_Integer)
new_esEs5(x0, x1, ty_Ordering)
new_esEs5(x0, x1, ty_Char)
new_esEs5(x0, x1, ty_Float)
new_esEs5(x0, x1, ty_Int)



↳ HASKELL
  ↳ IFR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                    ↳ DependencyGraphProof
                      ↳ AND
                        ↳ QDP
                        ↳ QDP
                          ↳ UsableRulesProof
                            ↳ QDP
                              ↳ QReductionProof
QDP
                                  ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_deleteBy0(xy10, xy11, xy12, False, ba, bb) → new_deleteBy(Left(xy12), xy10, ba, bb)
new_deleteBy(Left(xy30), :(Left(xy400), xy41), bc, bd) → new_deleteBy0(xy41, xy400, xy30, new_esEs4(xy30, xy400, bc), bc, bd)
new_deleteBy(Left(xy30), :(Right(xy400), xy41), bc, bd) → new_deleteBy(Left(xy30), xy41, bc, bd)

The TRS R consists of the following rules:

new_esEs4(xy30, xy400, ty_Int) → new_esEs7(xy30, xy400)
new_esEs4(xy30, xy400, ty_Char) → new_esEs21(xy30, xy400)
new_esEs4(xy30, xy400, ty_@0) → new_esEs20(xy30, xy400)
new_esEs4(xy30, xy400, ty_Float) → new_esEs6(xy30, xy400)
new_esEs4(xy30, xy400, ty_Double) → new_esEs19(xy30, xy400)
new_esEs4(xy30, xy400, app(ty_Ratio, gc)) → new_esEs14(xy30, xy400, gc)
new_esEs4(xy30, xy400, app(app(ty_Either, gg), gh)) → new_esEs22(xy30, xy400, gg, gh)
new_esEs4(xy30, xy400, app(app(ty_@2, gd), ge)) → new_esEs15(xy30, xy400, gd, ge)
new_esEs4(xy30, xy400, ty_Integer) → new_esEs12(xy30, xy400)
new_esEs4(xy30, xy400, ty_Bool) → new_esEs18(xy30, xy400)
new_esEs4(xy30, xy400, app(ty_[], gb)) → new_esEs13(xy30, xy400, gb)
new_esEs4(xy30, xy400, app(ty_Maybe, gf)) → new_esEs16(xy30, xy400, gf)
new_esEs4(xy30, xy400, ty_Ordering) → new_esEs17(xy30, xy400)
new_esEs4(xy30, xy400, app(app(app(ty_@3, bg), bh), ca)) → new_esEs8(xy30, xy400, bg, bh, ca)
new_esEs8(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), bg, bh, ca) → new_asAs(new_esEs11(xy300, xy4000, bg), new_asAs(new_esEs10(xy301, xy4001, bh), new_esEs9(xy302, xy4002, ca)))
new_esEs11(xy300, xy4000, ty_Int) → new_esEs7(xy300, xy4000)
new_esEs11(xy300, xy4000, ty_@0) → new_esEs20(xy300, xy4000)
new_esEs11(xy300, xy4000, ty_Char) → new_esEs21(xy300, xy4000)
new_esEs11(xy300, xy4000, app(ty_[], eg)) → new_esEs13(xy300, xy4000, eg)
new_esEs11(xy300, xy4000, app(app(ty_@2, fd), ff)) → new_esEs15(xy300, xy4000, fd, ff)
new_esEs11(xy300, xy4000, ty_Bool) → new_esEs18(xy300, xy4000)
new_esEs11(xy300, xy4000, ty_Float) → new_esEs6(xy300, xy4000)
new_esEs11(xy300, xy4000, app(ty_Ratio, fc)) → new_esEs14(xy300, xy4000, fc)
new_esEs11(xy300, xy4000, app(app(app(ty_@3, eh), fa), fb)) → new_esEs8(xy300, xy4000, eh, fa, fb)
new_esEs11(xy300, xy4000, app(ty_Maybe, fg)) → new_esEs16(xy300, xy4000, fg)
new_esEs11(xy300, xy4000, ty_Double) → new_esEs19(xy300, xy4000)
new_esEs11(xy300, xy4000, ty_Integer) → new_esEs12(xy300, xy4000)
new_esEs11(xy300, xy4000, ty_Ordering) → new_esEs17(xy300, xy4000)
new_esEs11(xy300, xy4000, app(app(ty_Either, fh), ga)) → new_esEs22(xy300, xy4000, fh, ga)
new_esEs10(xy301, xy4001, ty_Integer) → new_esEs12(xy301, xy4001)
new_esEs10(xy301, xy4001, app(app(app(ty_@3, df), dg), dh)) → new_esEs8(xy301, xy4001, df, dg, dh)
new_esEs10(xy301, xy4001, ty_Double) → new_esEs19(xy301, xy4001)
new_esEs10(xy301, xy4001, app(ty_[], de)) → new_esEs13(xy301, xy4001, de)
new_esEs10(xy301, xy4001, ty_Int) → new_esEs7(xy301, xy4001)
new_esEs10(xy301, xy4001, app(ty_Maybe, ed)) → new_esEs16(xy301, xy4001, ed)
new_esEs10(xy301, xy4001, ty_@0) → new_esEs20(xy301, xy4001)
new_esEs10(xy301, xy4001, ty_Ordering) → new_esEs17(xy301, xy4001)
new_esEs10(xy301, xy4001, ty_Bool) → new_esEs18(xy301, xy4001)
new_esEs10(xy301, xy4001, ty_Char) → new_esEs21(xy301, xy4001)
new_esEs10(xy301, xy4001, app(ty_Ratio, ea)) → new_esEs14(xy301, xy4001, ea)
new_esEs10(xy301, xy4001, app(app(ty_Either, ee), ef)) → new_esEs22(xy301, xy4001, ee, ef)
new_esEs10(xy301, xy4001, app(app(ty_@2, eb), ec)) → new_esEs15(xy301, xy4001, eb, ec)
new_esEs10(xy301, xy4001, ty_Float) → new_esEs6(xy301, xy4001)
new_esEs9(xy302, xy4002, app(ty_[], cb)) → new_esEs13(xy302, xy4002, cb)
new_esEs9(xy302, xy4002, ty_@0) → new_esEs20(xy302, xy4002)
new_esEs9(xy302, xy4002, ty_Float) → new_esEs6(xy302, xy4002)
new_esEs9(xy302, xy4002, ty_Char) → new_esEs21(xy302, xy4002)
new_esEs9(xy302, xy4002, ty_Integer) → new_esEs12(xy302, xy4002)
new_esEs9(xy302, xy4002, app(app(ty_Either, dc), dd)) → new_esEs22(xy302, xy4002, dc, dd)
new_esEs9(xy302, xy4002, app(app(ty_@2, cg), da)) → new_esEs15(xy302, xy4002, cg, da)
new_esEs9(xy302, xy4002, ty_Bool) → new_esEs18(xy302, xy4002)
new_esEs9(xy302, xy4002, app(ty_Ratio, cf)) → new_esEs14(xy302, xy4002, cf)
new_esEs9(xy302, xy4002, ty_Ordering) → new_esEs17(xy302, xy4002)
new_esEs9(xy302, xy4002, ty_Int) → new_esEs7(xy302, xy4002)
new_esEs9(xy302, xy4002, ty_Double) → new_esEs19(xy302, xy4002)
new_esEs9(xy302, xy4002, app(app(app(ty_@3, cc), cd), ce)) → new_esEs8(xy302, xy4002, cc, cd, ce)
new_esEs9(xy302, xy4002, app(ty_Maybe, db)) → new_esEs16(xy302, xy4002, db)
new_asAs(False, xy28) → False
new_asAs(True, xy28) → xy28
new_esEs16(Just(xy300), Just(xy4000), ty_Ordering) → new_esEs17(xy300, xy4000)
new_esEs16(Just(xy300), Just(xy4000), app(app(app(ty_@3, bgf), bgg), bgh)) → new_esEs8(xy300, xy4000, bgf, bgg, bgh)
new_esEs16(Nothing, Nothing, gf) → True
new_esEs16(Just(xy300), Just(xy4000), ty_Bool) → new_esEs18(xy300, xy4000)
new_esEs22(Right(xy300), Right(xy4000), gg, app(app(ty_Either, bce), bcf)) → new_esEs22(xy300, xy4000, bce, bcf)
new_esEs22(Right(xy300), Right(xy4000), gg, app(ty_Maybe, bcd)) → new_esEs16(xy300, xy4000, bcd)
new_esEs22(Left(xy300), Left(xy4000), app(app(ty_Either, bbc), bbd), gh) → new_esEs22(xy300, xy4000, bbc, bbd)
new_esEs22(Left(xy300), Left(xy4000), app(ty_Maybe, bbb), gh) → new_esEs16(xy300, xy4000, bbb)
new_esEs16(Just(xy300), Just(xy4000), app(ty_Maybe, bhd)) → new_esEs16(xy300, xy4000, bhd)
new_esEs16(Just(xy300), Just(xy4000), app(app(ty_Either, bhe), bhf)) → new_esEs22(xy300, xy4000, bhe, bhf)
new_esEs16(Just(xy300), Just(xy4000), ty_Char) → new_esEs21(xy300, xy4000)
new_esEs16(Just(xy300), Just(xy4000), ty_Integer) → new_esEs12(xy300, xy4000)
new_esEs16(Just(xy300), Just(xy4000), app(app(ty_@2, bhb), bhc)) → new_esEs15(xy300, xy4000, bhb, bhc)
new_esEs16(Just(xy300), Just(xy4000), ty_@0) → new_esEs20(xy300, xy4000)
new_esEs16(Just(xy300), Just(xy4000), ty_Float) → new_esEs6(xy300, xy4000)
new_esEs16(Just(xy300), Just(xy4000), ty_Int) → new_esEs7(xy300, xy4000)
new_esEs16(Nothing, Just(xy4000), gf) → False
new_esEs16(Just(xy300), Nothing, gf) → False
new_esEs16(Just(xy300), Just(xy4000), app(ty_[], bge)) → new_esEs13(xy300, xy4000, bge)
new_esEs16(Just(xy300), Just(xy4000), ty_Double) → new_esEs19(xy300, xy4000)
new_esEs16(Just(xy300), Just(xy4000), app(ty_Ratio, bha)) → new_esEs14(xy300, xy4000, bha)
new_esEs14(:%(xy300, xy301), :%(xy4000, xy4001), gc) → new_asAs(new_esEs24(xy300, xy4000, gc), new_esEs23(xy301, xy4001, gc))
new_esEs24(xy300, xy4000, ty_Integer) → new_esEs12(xy300, xy4000)
new_esEs24(xy300, xy4000, ty_Int) → new_esEs7(xy300, xy4000)
new_esEs23(xy301, xy4001, ty_Int) → new_esEs7(xy301, xy4001)
new_esEs23(xy301, xy4001, ty_Integer) → new_esEs12(xy301, xy4001)
new_esEs12(Integer(xy300), Integer(xy4000)) → new_primEqInt(xy300, xy4000)
new_primEqInt(Neg(Succ(xy3000)), Pos(xy4000)) → False
new_primEqInt(Pos(Succ(xy3000)), Neg(xy4000)) → False
new_primEqInt(Neg(Zero), Pos(Succ(xy40000))) → False
new_primEqInt(Pos(Zero), Neg(Succ(xy40000))) → False
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_primEqInt(Neg(Succ(xy3000)), Neg(Succ(xy40000))) → new_primEqNat0(xy3000, xy40000)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_primEqInt(Neg(Zero), Neg(Succ(xy40000))) → False
new_primEqInt(Neg(Succ(xy3000)), Neg(Zero)) → False
new_primEqInt(Pos(Succ(xy3000)), Pos(Succ(xy40000))) → new_primEqNat0(xy3000, xy40000)
new_primEqInt(Pos(Succ(xy3000)), Pos(Zero)) → False
new_primEqInt(Pos(Zero), Pos(Succ(xy40000))) → False
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_primEqNat0(Succ(xy3000), Zero) → False
new_primEqNat0(Zero, Succ(xy40000)) → False
new_primEqNat0(Zero, Zero) → True
new_primEqNat0(Succ(xy3000), Succ(xy40000)) → new_primEqNat0(xy3000, xy40000)
new_esEs7(xy30, xy400) → new_primEqInt(xy30, xy400)
new_esEs19(Double(xy300, xy301), Double(xy4000, xy4001)) → new_esEs7(new_sr(xy300, xy4000), new_sr(xy301, xy4001))
new_sr(Pos(xy3010), Neg(xy40010)) → Neg(new_primMulNat0(xy3010, xy40010))
new_sr(Neg(xy3010), Pos(xy40010)) → Neg(new_primMulNat0(xy3010, xy40010))
new_sr(Neg(xy3010), Neg(xy40010)) → Pos(new_primMulNat0(xy3010, xy40010))
new_sr(Pos(xy3010), Pos(xy40010)) → Pos(new_primMulNat0(xy3010, xy40010))
new_primMulNat0(Zero, Zero) → Zero
new_primMulNat0(Succ(xy30100), Zero) → Zero
new_primMulNat0(Zero, Succ(xy400100)) → Zero
new_primMulNat0(Succ(xy30100), Succ(xy400100)) → new_primPlusNat0(new_primMulNat0(xy30100, Succ(xy400100)), xy400100)
new_primPlusNat0(Zero, xy400100) → Succ(xy400100)
new_primPlusNat0(Succ(xy290), xy400100) → Succ(Succ(new_primPlusNat1(xy290, xy400100)))
new_primPlusNat1(Succ(xy2900), Succ(xy4001000)) → Succ(Succ(new_primPlusNat1(xy2900, xy4001000)))
new_primPlusNat1(Zero, Succ(xy4001000)) → Succ(xy4001000)
new_primPlusNat1(Succ(xy2900), Zero) → Succ(xy2900)
new_primPlusNat1(Zero, Zero) → Zero
new_esEs13([], [], gb) → True
new_esEs13([], :(xy4000, xy4001), gb) → False
new_esEs13(:(xy300, xy301), [], gb) → False
new_esEs13(:(xy300, xy301), :(xy4000, xy4001), gb) → new_asAs(new_esEs25(xy300, xy4000, gb), new_esEs13(xy301, xy4001, gb))
new_esEs25(xy300, xy4000, ty_Ordering) → new_esEs17(xy300, xy4000)
new_esEs25(xy300, xy4000, ty_Integer) → new_esEs12(xy300, xy4000)
new_esEs25(xy300, xy4000, app(app(ty_@2, hf), hg)) → new_esEs15(xy300, xy4000, hf, hg)
new_esEs25(xy300, xy4000, ty_Int) → new_esEs7(xy300, xy4000)
new_esEs25(xy300, xy4000, app(app(ty_Either, baa), bab)) → new_esEs22(xy300, xy4000, baa, bab)
new_esEs25(xy300, xy4000, app(app(app(ty_@3, hb), hc), hd)) → new_esEs8(xy300, xy4000, hb, hc, hd)
new_esEs25(xy300, xy4000, app(ty_Ratio, he)) → new_esEs14(xy300, xy4000, he)
new_esEs25(xy300, xy4000, ty_Float) → new_esEs6(xy300, xy4000)
new_esEs25(xy300, xy4000, ty_Bool) → new_esEs18(xy300, xy4000)
new_esEs25(xy300, xy4000, app(ty_[], ha)) → new_esEs13(xy300, xy4000, ha)
new_esEs25(xy300, xy4000, ty_Char) → new_esEs21(xy300, xy4000)
new_esEs25(xy300, xy4000, ty_Double) → new_esEs19(xy300, xy4000)
new_esEs25(xy300, xy4000, app(ty_Maybe, hh)) → new_esEs16(xy300, xy4000, hh)
new_esEs25(xy300, xy4000, ty_@0) → new_esEs20(xy300, xy4000)
new_esEs20(@0, @0) → True
new_esEs21(Char(xy300), Char(xy4000)) → new_primEqNat0(xy300, xy4000)
new_esEs18(True, True) → True
new_esEs18(True, False) → False
new_esEs18(False, True) → False
new_esEs18(False, False) → True
new_esEs6(Float(xy300, xy301), Float(xy4000, xy4001)) → new_esEs7(new_sr(xy300, xy4000), new_sr(xy301, xy4001))
new_esEs22(Right(xy300), Right(xy4000), gg, ty_Ordering) → new_esEs17(xy300, xy4000)
new_esEs22(Left(xy300), Left(xy4000), ty_Float, gh) → new_esEs6(xy300, xy4000)
new_esEs22(Left(xy300), Left(xy4000), ty_Char, gh) → new_esEs21(xy300, xy4000)
new_esEs22(Right(xy300), Right(xy4000), gg, app(app(ty_@2, bcb), bcc)) → new_esEs15(xy300, xy4000, bcb, bcc)
new_esEs22(Left(xy300), Left(xy4000), ty_@0, gh) → new_esEs20(xy300, xy4000)
new_esEs22(Left(xy300), Left(xy4000), ty_Int, gh) → new_esEs7(xy300, xy4000)
new_esEs22(Left(xy300), Left(xy4000), app(app(ty_@2, bah), bba), gh) → new_esEs15(xy300, xy4000, bah, bba)
new_esEs22(Left(xy300), Left(xy4000), app(ty_[], bac), gh) → new_esEs13(xy300, xy4000, bac)
new_esEs22(Right(xy300), Right(xy4000), gg, app(app(app(ty_@3, bbf), bbg), bbh)) → new_esEs8(xy300, xy4000, bbf, bbg, bbh)
new_esEs22(Right(xy300), Right(xy4000), gg, ty_Float) → new_esEs6(xy300, xy4000)
new_esEs22(Right(xy300), Right(xy4000), gg, ty_Char) → new_esEs21(xy300, xy4000)
new_esEs22(Left(xy300), Left(xy4000), ty_Ordering, gh) → new_esEs17(xy300, xy4000)
new_esEs22(Left(xy300), Left(xy4000), ty_Integer, gh) → new_esEs12(xy300, xy4000)
new_esEs22(Left(xy300), Left(xy4000), app(ty_Ratio, bag), gh) → new_esEs14(xy300, xy4000, bag)
new_esEs22(Right(xy300), Right(xy4000), gg, ty_Int) → new_esEs7(xy300, xy4000)
new_esEs22(Right(xy300), Right(xy4000), gg, ty_Double) → new_esEs19(xy300, xy4000)
new_esEs22(Left(xy300), Left(xy4000), ty_Double, gh) → new_esEs19(xy300, xy4000)
new_esEs22(Right(xy300), Right(xy4000), gg, ty_Integer) → new_esEs12(xy300, xy4000)
new_esEs22(Right(xy300), Right(xy4000), gg, ty_Bool) → new_esEs18(xy300, xy4000)
new_esEs22(Left(xy300), Left(xy4000), app(app(app(ty_@3, bad), bae), baf), gh) → new_esEs8(xy300, xy4000, bad, bae, baf)
new_esEs22(Right(xy300), Right(xy4000), gg, app(ty_Ratio, bca)) → new_esEs14(xy300, xy4000, bca)
new_esEs22(Left(xy300), Left(xy4000), ty_Bool, gh) → new_esEs18(xy300, xy4000)
new_esEs22(Right(xy300), Left(xy4000), gg, gh) → False
new_esEs22(Left(xy300), Right(xy4000), gg, gh) → False
new_esEs22(Right(xy300), Right(xy4000), gg, ty_@0) → new_esEs20(xy300, xy4000)
new_esEs22(Right(xy300), Right(xy4000), gg, app(ty_[], bbe)) → new_esEs13(xy300, xy4000, bbe)
new_esEs17(LT, LT) → True
new_esEs17(LT, EQ) → False
new_esEs17(EQ, LT) → False
new_esEs17(EQ, EQ) → True
new_esEs17(GT, GT) → True
new_esEs17(LT, GT) → False
new_esEs17(GT, LT) → False
new_esEs17(EQ, GT) → False
new_esEs17(GT, EQ) → False
new_esEs15(@2(xy300, xy301), @2(xy4000, xy4001), gd, ge) → new_asAs(new_esEs27(xy300, xy4000, gd), new_esEs26(xy301, xy4001, ge))
new_esEs27(xy300, xy4000, app(app(ty_@2, bfh), bga)) → new_esEs15(xy300, xy4000, bfh, bga)
new_esEs27(xy300, xy4000, ty_Integer) → new_esEs12(xy300, xy4000)
new_esEs27(xy300, xy4000, app(app(ty_Either, bgc), bgd)) → new_esEs22(xy300, xy4000, bgc, bgd)
new_esEs27(xy300, xy4000, app(ty_Maybe, bgb)) → new_esEs16(xy300, xy4000, bgb)
new_esEs27(xy300, xy4000, app(ty_Ratio, bfg)) → new_esEs14(xy300, xy4000, bfg)
new_esEs27(xy300, xy4000, ty_Int) → new_esEs7(xy300, xy4000)
new_esEs27(xy300, xy4000, ty_Float) → new_esEs6(xy300, xy4000)
new_esEs27(xy300, xy4000, ty_@0) → new_esEs20(xy300, xy4000)
new_esEs27(xy300, xy4000, ty_Char) → new_esEs21(xy300, xy4000)
new_esEs27(xy300, xy4000, ty_Ordering) → new_esEs17(xy300, xy4000)
new_esEs27(xy300, xy4000, ty_Bool) → new_esEs18(xy300, xy4000)
new_esEs27(xy300, xy4000, app(ty_[], bfc)) → new_esEs13(xy300, xy4000, bfc)
new_esEs27(xy300, xy4000, app(app(app(ty_@3, bfd), bfe), bff)) → new_esEs8(xy300, xy4000, bfd, bfe, bff)
new_esEs27(xy300, xy4000, ty_Double) → new_esEs19(xy300, xy4000)
new_esEs26(xy301, xy4001, ty_Bool) → new_esEs18(xy301, xy4001)
new_esEs26(xy301, xy4001, app(app(ty_@2, bef), beg)) → new_esEs15(xy301, xy4001, bef, beg)
new_esEs26(xy301, xy4001, app(ty_Ratio, bee)) → new_esEs14(xy301, xy4001, bee)
new_esEs26(xy301, xy4001, ty_Float) → new_esEs6(xy301, xy4001)
new_esEs26(xy301, xy4001, app(app(app(ty_@3, beb), bec), bed)) → new_esEs8(xy301, xy4001, beb, bec, bed)
new_esEs26(xy301, xy4001, ty_Int) → new_esEs7(xy301, xy4001)
new_esEs26(xy301, xy4001, ty_Double) → new_esEs19(xy301, xy4001)
new_esEs26(xy301, xy4001, ty_Integer) → new_esEs12(xy301, xy4001)
new_esEs26(xy301, xy4001, app(ty_[], bea)) → new_esEs13(xy301, xy4001, bea)
new_esEs26(xy301, xy4001, ty_Ordering) → new_esEs17(xy301, xy4001)
new_esEs26(xy301, xy4001, app(app(ty_Either, bfa), bfb)) → new_esEs22(xy301, xy4001, bfa, bfb)
new_esEs26(xy301, xy4001, app(ty_Maybe, beh)) → new_esEs16(xy301, xy4001, beh)
new_esEs26(xy301, xy4001, ty_@0) → new_esEs20(xy301, xy4001)
new_esEs26(xy301, xy4001, ty_Char) → new_esEs21(xy301, xy4001)

The set Q consists of the following terms:

new_esEs10(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs17(LT, GT)
new_esEs17(GT, LT)
new_esEs27(x0, x1, app(app(ty_@2, x2), x3))
new_esEs4(x0, x1, app(ty_[], x2))
new_esEs27(x0, x1, app(ty_[], x2))
new_esEs12(Integer(x0), Integer(x1))
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs11(x0, x1, ty_Bool)
new_esEs22(Right(x0), Right(x1), x2, ty_@0)
new_esEs4(x0, x1, ty_Bool)
new_esEs16(Just(x0), Just(x1), app(ty_Maybe, x2))
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_esEs27(x0, x1, ty_@0)
new_esEs22(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs22(Right(x0), Right(x1), x2, ty_Int)
new_esEs17(LT, LT)
new_esEs27(x0, x1, ty_Float)
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_esEs16(Just(x0), Just(x1), ty_Ordering)
new_esEs14(:%(x0, x1), :%(x2, x3), x4)
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs9(x0, x1, ty_Int)
new_esEs4(x0, x1, ty_Double)
new_esEs10(x0, x1, ty_Ordering)
new_esEs18(False, True)
new_esEs18(True, False)
new_asAs(False, x0)
new_esEs10(x0, x1, app(app(ty_Either, x2), x3))
new_primPlusNat1(Succ(x0), Zero)
new_esEs9(x0, x1, ty_Bool)
new_esEs25(x0, x1, ty_Double)
new_esEs16(Just(x0), Just(x1), app(ty_[], x2))
new_primEqInt(Neg(Zero), Neg(Zero))
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs4(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_Integer)
new_esEs7(x0, x1)
new_esEs9(x0, x1, ty_Integer)
new_esEs22(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs11(x0, x1, ty_Ordering)
new_esEs13([], [], x0)
new_esEs9(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs17(EQ, GT)
new_esEs17(GT, EQ)
new_esEs22(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs22(Left(x0), Left(x1), ty_Double, x2)
new_esEs9(x0, x1, app(app(ty_@2, x2), x3))
new_esEs11(x0, x1, ty_Float)
new_esEs9(x0, x1, app(ty_Ratio, x2))
new_esEs11(x0, x1, app(app(ty_@2, x2), x3))
new_esEs22(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs27(x0, x1, ty_Integer)
new_esEs27(x0, x1, ty_Ordering)
new_esEs18(True, True)
new_esEs26(x0, x1, ty_Double)
new_esEs26(x0, x1, ty_Integer)
new_primPlusNat1(Zero, Succ(x0))
new_esEs16(Just(x0), Just(x1), ty_Double)
new_primPlusNat0(Zero, x0)
new_esEs25(x0, x1, ty_Float)
new_esEs26(x0, x1, ty_Int)
new_esEs10(x0, x1, app(ty_Maybe, x2))
new_esEs16(Nothing, Nothing, x0)
new_esEs8(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_asAs(True, x0)
new_esEs25(x0, x1, ty_Bool)
new_esEs16(Just(x0), Just(x1), ty_Float)
new_esEs17(GT, GT)
new_esEs25(x0, x1, ty_Int)
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_esEs4(x0, x1, ty_Char)
new_esEs11(x0, x1, ty_Int)
new_esEs27(x0, x1, ty_Int)
new_esEs4(x0, x1, ty_Integer)
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs25(x0, x1, ty_Integer)
new_esEs9(x0, x1, ty_Double)
new_esEs22(Right(x0), Right(x1), x2, ty_Bool)
new_esEs26(x0, x1, ty_Bool)
new_esEs25(x0, x1, ty_Char)
new_sr(Pos(x0), Pos(x1))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs22(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs10(x0, x1, app(app(ty_@2, x2), x3))
new_primEqNat0(Zero, Zero)
new_esEs24(x0, x1, ty_Int)
new_esEs24(x0, x1, ty_Integer)
new_esEs22(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs4(x0, x1, ty_Float)
new_esEs9(x0, x1, ty_Char)
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs22(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs16(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs22(Right(x0), Right(x1), x2, ty_Float)
new_primEqNat0(Zero, Succ(x0))
new_esEs10(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_Int)
new_esEs22(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs10(x0, x1, ty_Char)
new_esEs6(Float(x0, x1), Float(x2, x3))
new_esEs27(x0, x1, app(ty_Ratio, x2))
new_esEs11(x0, x1, app(app(ty_Either, x2), x3))
new_esEs13(:(x0, x1), [], x2)
new_esEs22(Left(x0), Left(x1), ty_@0, x2)
new_esEs9(x0, x1, ty_@0)
new_primMulNat0(Zero, Zero)
new_esEs25(x0, x1, ty_@0)
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs19(Double(x0, x1), Double(x2, x3))
new_esEs22(Left(x0), Left(x1), ty_Bool, x2)
new_esEs22(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs9(x0, x1, ty_Float)
new_esEs26(x0, x1, ty_Char)
new_esEs9(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs16(Just(x0), Just(x1), ty_@0)
new_esEs9(x0, x1, ty_Ordering)
new_esEs13([], :(x0, x1), x2)
new_esEs10(x0, x1, ty_Float)
new_esEs27(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs22(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs11(x0, x1, app(ty_[], x2))
new_esEs16(Nothing, Just(x0), x1)
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_esEs9(x0, x1, app(ty_Maybe, x2))
new_esEs26(x0, x1, app(ty_[], x2))
new_esEs10(x0, x1, app(ty_Ratio, x2))
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs27(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, ty_Ordering)
new_esEs22(Left(x0), Left(x1), ty_Integer, x2)
new_esEs16(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_esEs21(Char(x0), Char(x1))
new_esEs15(@2(x0, x1), @2(x2, x3), x4, x5)
new_primMulNat0(Zero, Succ(x0))
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs11(x0, x1, ty_Char)
new_esEs22(Right(x0), Right(x1), x2, ty_Integer)
new_esEs27(x0, x1, ty_Char)
new_esEs11(x0, x1, ty_@0)
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs16(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs22(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs22(Left(x0), Left(x1), ty_Char, x2)
new_esEs16(Just(x0), Just(x1), ty_Integer)
new_esEs10(x0, x1, ty_Integer)
new_esEs18(False, False)
new_esEs27(x0, x1, ty_Double)
new_esEs20(@0, @0)
new_esEs16(Just(x0), Just(x1), ty_Int)
new_esEs22(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs4(x0, x1, ty_Ordering)
new_esEs22(Right(x0), Right(x1), x2, ty_Char)
new_esEs11(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs26(x0, x1, ty_@0)
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs22(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs13(:(x0, x1), :(x2, x3), x4)
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs11(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs10(x0, x1, ty_Bool)
new_primEqNat0(Succ(x0), Zero)
new_sr(Neg(x0), Neg(x1))
new_esEs10(x0, x1, ty_Double)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_primPlusNat1(Zero, Zero)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs27(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(Left(x0), Left(x1), ty_Int, x2)
new_esEs4(x0, x1, ty_Int)
new_esEs16(Just(x0), Nothing, x1)
new_esEs22(Left(x0), Right(x1), x2, x3)
new_esEs22(Right(x0), Left(x1), x2, x3)
new_primEqInt(Pos(Zero), Pos(Zero))
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs11(x0, x1, app(ty_Maybe, x2))
new_primPlusNat0(Succ(x0), x1)
new_esEs26(x0, x1, ty_Ordering)
new_esEs22(Right(x0), Right(x1), x2, ty_Double)
new_esEs17(EQ, EQ)
new_esEs17(EQ, LT)
new_esEs17(LT, EQ)
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs11(x0, x1, ty_Double)
new_esEs16(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs22(Left(x0), Left(x1), ty_Float, x2)
new_esEs10(x0, x1, ty_Int)
new_esEs16(Just(x0), Just(x1), ty_Bool)
new_esEs9(x0, x1, app(ty_[], x2))
new_esEs26(x0, x1, ty_Float)
new_esEs27(x0, x1, ty_Bool)
new_primMulNat0(Succ(x0), Zero)
new_esEs10(x0, x1, app(ty_[], x2))
new_esEs11(x0, x1, ty_Integer)
new_esEs16(Just(x0), Just(x1), ty_Char)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: